search

imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

What commit of fcsl-pcm works with coq 8.12? #37

Closed brando90 closed 1 year ago

brando90 commented 1 year ago

I think 1.3.0 and thus this commit might work 8443f7e35f70c73b6185beeab427d516feb43747. Actually, maybe this one fab4dfe3ca58ecf8aefeb8fa4ac4a2659b231f24.

brando90 commented 1 year ago

yes this worked!

(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/fcsl-pcm && git checkout fab4dfe3ca58ecf8aefeb8fa4ac4a2659b231f24 && git rev-parse HEAD)
Previous HEAD position was 8443f7e 1.3 updates
HEAD is now at fab4dfe fcsl-pcm is compatible with Coq 8.12
fab4dfe3ca58ecf8aefeb8fa4ac4a2659b231f24
(iit_synthesis) brando9~/proverbot9001 $ opam switch
#  switch    compiler                    description
   coq-8.10  ocaml-base-compiler.4.07.1  coq-8.10
→  coq-8.12  ocaml-base-compiler.4.07.1  coq-8.12
   default   ocaml.5.0.0                 default
(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/fcsl-pcm && make "$@" && make install)
coq_makefile -f _CoqProject -o CoqMakefile
make --no-print-directory -f CoqMakefile
COQDEP VFILES
COQC finmap/ordtype.v
COQC finmap/finmap.v
COQC pcm/pred.v
COQC pcm/pcm.v
COQC pcm/unionmap.v
COQC pcm/automap.v
COQC pcm/axioms.v
COQC pcm/heap.v
COQC pcm/prelude.v
COQC pcm/mutex.v
COQC pcm/lift.v
COQC pcm/natmap.v
coq_makefile -f _CoqProject -o CoqMakefile
make --no-print-directory -f CoqMakefile install
INSTALL finmap/finmap.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//finmap
INSTALL finmap/ordtype.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//finmap
INSTALL pcm/automap.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/axioms.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/heap.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/mutex.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/lift.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/natmap.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/pcm.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/pred.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/prelude.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/unionmap.vo /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL finmap/finmap.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//finmap
INSTALL finmap/ordtype.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//finmap
INSTALL pcm/automap.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/axioms.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/heap.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/mutex.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/lift.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/natmap.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/pcm.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/pred.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/prelude.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/unionmap.v /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL finmap/finmap.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//finmap
INSTALL finmap/ordtype.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//finmap
INSTALL pcm/automap.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/axioms.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/heap.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/mutex.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/lift.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/natmap.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/pcm.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/pred.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/prelude.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm
INSTALL pcm/unionmap.glob /lfs/ampere2/0/brando9/.opam/coq-8.12/lib/coq//user-contrib/fcsl//pcm