search

UCSD-PL / proverbot9001

GNU General Public License v3.0
39 stars 17 forks source link

final command (cd coq-projects/fcsl-pcm && make "$@" && make install) doesn't seem to work for coq 8.12, what to do? #94

Closed brando90 closed 1 year ago

brando90 commented 1 year ago

I did:

(iit_synthesis) brando9~/proverbot9001 $ git clone git@github.com/imdea-software/fcsl-pcm deps/fcsl-pcm
fatal: repository 'git@github.com/imdea-software/fcsl-pcm' does not exist
(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/fcsl-pcm && make "$@" && make install)
coq_makefile -f _CoqProject -o CoqMakefile
make --no-print-directory -f CoqMakefile
COQC core/prelude.v
File "./core/prelude.v", line 222, characters 0-94:
Error: This command does not support this attribute: export.
[unsupported-attributes,parsing]

make[2]: *** [CoqMakefile:716: core/prelude.vo] Error 1
make[1]: *** [CoqMakefile:339: all] Error 2
make: *** [Makefile:13: invoke-coqmakefile] Error 2

what to do for coq 8.12?

brando90 commented 1 year ago

if final answer by Alex doesn't help then likely only solution is to:

  1. when building the projects, whichever depends on cheerios, verdi coq 8.12 switch, upgrade to a version were those two work e.g. 8.14+ likely most recent is what I'd go with
  2. create out own forks that support 8.12. Likely option 1 is better.

though I am going through some of the version e.g. 

opam install -y coq-fcsl-pcm=1.3.0

and if that works perhaps I can cd into the directory and request that request in the opam install or get the commit that uses that version.

brando90 commented 1 year ago

ok I think I found a commit that works: https://github.com/imdea-software/fcsl-pcm/issues/37

brando90 commented 1 year ago

running this:

# Install fcsl-pcm
git clone git@github.com:imdea-software/fcsl-pcm.git coq-projects/fcsl-pcm
(cd coq-projects/fcsl-pcm && make "$@" && make install)
(cd coq-projects/fcsl-pcm && git checkout fab4dfe3ca58ecf8aefeb8fa4ac4a2659b231f24 && git rev-parse HEAD)
#(cd coq-projects/fcsl-pcm && opam install -y .)
#(cd coq-projects/fcsl-pcm && opam install -y --ignore-constraints-on=coq .)

gives no errors:

(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
brando90 commented 1 year ago

going to try (cd coq-projects/fcsl-pcm && opam install -y .) and see if that works.

Seems to have worked:

(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/fcsl-pcm && git checkout fab4dfe3ca58ecf8aefeb8fa4ac4a2659b231f24 && git rev-parse HEAD)
HEAD is now at fab4dfe fcsl-pcm is compatible with Coq 8.12
fab4dfe3ca58ecf8aefeb8fa4ac4a2659b231f24
(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/fcsl-pcm && opam install -y .)
[coq-fcsl-pcm.dev] synchronised (git+file:///afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/fcsl-pcm#HEAD)
The following actions will be performed:
  ↻ recompile coq-fcsl-pcm dev*

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⊘ removed   coq-fcsl-pcm.dev
∗ installed coq-fcsl-pcm.dev
Done.

So either is fine, make or opam (I hope). Can't tell until later build...