Issues
- 0
Hyperparameters from file
#126 opened by HazardousPeach - 1
Result about Coqgym
#123 opened by liuxingpeng520521 - 5
Number of extractable proofs and matched proofs?
#112 opened by jizej - 2
Some other metric of your lastest results
#122 opened by liuxingpeng520521 - 1
The result in compcert.
#117 opened by liuxingpeng520521 - 1
Pin versions in requirements.txt
#116 opened by mizlan - 1
Update instructions for macOS arm64: include directory
#115 opened by mizlan - 1
sharing the already build opam environment?
#84 opened by brando90 - 7
deps/verdi doesn't seem to work for coq 8.12 even with the --ignore-constraints-on=coq trick, is it really needed?
#93 opened by brando90 - 5
search-report fails on the pinned math-comp version. coq_serapy.CoqExn: Expected prenex implicits for tag_of_pairK
#97 opened by aleloi - 3
Is the .gitmodules file incomplete -- e.g. it's misisng constructive-geometry coq project?
#98 opened by brando90 - 2
writing the opam activation env without relative paths in build_coq_projects.sh
#99 opened by brando90 - 3
Some packages that don't have an official opam repository version don't need commit hashes -- InfSeqExt?
#91 opened by brando90 - 2
How to install metalib so that is fully compatible with proverbot9001 dependency install?
#86 opened by brando90 - 1
stable tag for menhir for coq 8.12
#89 opened by brando90 - 6
Some packages that don't have an official opam repository version don't need commit hashes -- StructTact?
#90 opened by brando90 - 1
installing verdi and cheerios for coq 8.10 -- getting their commits for opam pin after updates to these repos overwrite the OPAM online repository
#85 opened by brando90 - 7
current deps/cheerios for coq 8.12 really works?
#92 opened by brando90 - 4
- 4
final command (cd coq-projects/fcsl-pcm && make "$@" && make install) doesn't seem to work for coq 8.12, what to do?
#94 opened by brando90 - 1
- 3
Some coq packages for coq 8.12 don't exist anymore? coq-smpl=8.12 coq-metacoq-template coq-metacoq-checker
#88 opened by brando90 - 14
why does metalib need coq 8.15 and how to fix it so that it compatible with proverbot9001 -- do we need coq-8.10 really?
#82 opened by brando90 - 20
metalib is missing even after git submodule update && git submodule init command
#59 opened by brando90 - 13
installing deps for coq doesn't work, need >=8.14 not 8.10, most likely coq-cheerios and verdi - help fix!
#78 opened by brando90 - 6
install_coqgym_deps.sh fails when running giant opam install -- due to coq-cheerios (only tried coq-cheerios)
#55 opened by brando90 - 8
- 1
- 1
Why is proverbot asking me for a username and password when I try to initialize the coq-projects using gitsubmodules commands?
#74 opened by brando90 - 32
lin-alg fails to install with current instructions `(cd coq-projects/lin-alg && make "$@" && make install)`
#61 opened by brando90 - 2
- 4
coq lin-alg-8.10 seems to install (with coq 8.9 or 8.10?) but doesn't appear in opam list
#81 opened by brando90 - 2
Unable to get coq_serapy
#76 opened by brando90 - 2
coq cherios fails also in deps
#64 opened by brando90 - 2
how are you making sure each coq-proj is pinned to a specific git commit and doesn't break your setup?
#80 opened by brando90 - 1
- 3
- 7
metalib requires coq 8.15, what to do? I think we might need to also save the commit of each coq project we submodule e.g. in the splits .json file
#60 opened by brando90 - 1
why are you doing gitsubmodule update then git submodule init -- isn't the reverse the standard?
#71 opened by brando90 - 1
curious, is the coq standard library included in coq-projects? if not how can we include it?
#70 opened by brando90 - 1
can one make a data set without downloading the source files e.g. just downloading from a specific version of the coq-proj from opam install?
#69 opened by brando90 - 1
is it possible to get ride of the .modules git file and have everything in a coq_proj.opam file?
#68 opened by brando90 - 1
when `configure x86_64-linux `needed?
#67 opened by brando90 - 8
what is the `configure` command e.g. when building CompCert? Are there other unexpected commands like that needed during the compiling process of each coq proj?
#65 opened by brando90 - 4
- 3
Installing verdi is confusing
#57 opened by brando90 - 3
original instruction to install of package coq-ext-lib fails with the 8.10 switch
#56 opened by brando90 - 1
when to use remake? e.g. coquelicot uses remake instead of make clean -C path2coq_proj
#66 opened by brando90 - 1
some commands suggest #opam repository add coq-released --all-switches should we do it?
#63 opened by brando90 - 1
what things need to be "copied" as git submodules and what things are ok just to opam install/pin?
#62 opened by brando90