Skip to content

Latest commit

 

History

History

bench

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
README.md
README.md
 
 
_CoqProject
_CoqProject
 
 
asymptotics.agda
asymptotics.agda
 
 
asymptotics.idr
asymptotics.idr
 
 
asymptotics.lean
asymptotics.lean
 
 
asymptotics.stt
asymptotics.stt
 
 
asymptotics.v
asymptotics.v
 
 
conv_eval.agda
conv_eval.agda
 
 
conv_eval.idr
conv_eval.idr
 
 
conv_eval.lean
conv_eval.lean
 
 
conv_eval.stt
conv_eval.stt
 
 
conv_eval.v
conv_eval.v
 
 
stlc.agda
stlc.agda
 
 
stlc.idr
stlc.idr
 
 
stlc.lean
stlc.lean
 
 
stlc.stt
stlc.stt
 
 
stlc100k.lean
stlc100k.lean
 
 
stlc100k.stt
stlc100k.stt
 
 
stlc10k.agda
stlc10k.agda
 
 
stlc10k.idr
stlc10k.idr
 
 
stlc10k.lean
stlc10k.lean
 
 
stlc10k.stt
stlc10k.stt
 
 
stlc1k.agda
stlc1k.agda
 
 
stlc1k.lean
stlc1k.lean
 
 
stlc5k.agda
stlc5k.agda
 
 
stlc5k.idr
stlc5k.idr
 
 
stlc5k.lean
stlc5k.lean
 
 
stlc5k.stt
stlc5k.stt
 
 
stlc_lessimpl.agda
stlc_lessimpl.agda
 
 
stlc_lessimpl.idr
stlc_lessimpl.idr
 
 
stlc_lessimpl.lean
stlc_lessimpl.lean
 
 
stlc_lessimpl.stt
stlc_lessimpl.stt
 
 
stlc_lessimpl.v
stlc_lessimpl.v
 
 
stlc_lessimpl10k.agda
stlc_lessimpl10k.agda
 
 
stlc_lessimpl10k.idr
stlc_lessimpl10k.idr
 
 
stlc_lessimpl10k.lean
stlc_lessimpl10k.lean
 
 
stlc_lessimpl10k.stt
stlc_lessimpl10k.stt
 
 
stlc_lessimpl10k.v
stlc_lessimpl10k.v
 
 
stlc_lessimpl5k.agda
stlc_lessimpl5k.agda
 
 
stlc_lessimpl5k.idr
stlc_lessimpl5k.idr
 
 
stlc_lessimpl5k.lean
stlc_lessimpl5k.lean
 
 
stlc_lessimpl5k.stt
stlc_lessimpl5k.stt
 
 
stlc_lessimpl5k.v
stlc_lessimpl5k.v
 
 
stlc_small.agda
stlc_small.agda
 
 
stlc_small.idr
stlc_small.idr
 
 
stlc_small.lean
stlc_small.lean
 
 
stlc_small.stt
stlc_small.stt
 
 
stlc_small.v
stlc_small.v
 
 
stlc_small10k.agda
stlc_small10k.agda
 
 
stlc_small10k.idr
stlc_small10k.idr
 
 
stlc_small10k.lean
stlc_small10k.lean
 
 
stlc_small10k.stt
stlc_small10k.stt
 
 
stlc_small10k.v
stlc_small10k.v
 
 
stlc_small1k.idr
stlc_small1k.idr
 
 
stlc_small2k.idr
stlc_small2k.idr
 
 
stlc_small5k.agda
stlc_small5k.agda
 
 
stlc_small5k.idr
stlc_small5k.idr
 
 
stlc_small5k.lean
stlc_small5k.lean
 
 
stlc_small5k.stt
stlc_small5k.stt
 
 
stlc_small5k.v
stlc_small5k.v
 
 

README.md

commands

  • agda: agda FILE -vprofile:7 +RTS -M10G
  • coq: time coqtop -l FILE -batch -type-in-type -time or without -time if we're benchmarking elaboration.
  • lean:
    • grab the correct Lean path with elan which lean
    • su
    • ulimit -s unlimited
    • lean FILE --profile where lean is the path we got
  • idris2: time idris2 -c FILE