Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Error when installing #10

Closed
BoltonBailey opened this issue Oct 27, 2020 · 1 comment
Closed

Error when installing #10

BoltonBailey opened this issue Oct 27, 2020 · 1 comment

Comments

@BoltonBailey
Copy link

I tried to install this project using the instructions in the readme. This is the terminal output I got:

21:56:27 Project #=# mkdir coqgym
21:56:45 Project #=# cd coqgym
21:56:50 coqgym #=# opam switch create 4.07.1+flambda && eval $(opam env)

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
[ocaml-variants.4.07.1+flambda] downloaded from cache at https://opam.ocaml.org/cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫 
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-variants.4.07.1+flambda
∗ installed ocaml-config.1
∗ installed ocaml.4.07.1
Done.
# Run eval $(opam env) to update the current shell environment
21:59:48 coqgym #=# opam upgrade && eval $(opam env)
Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
However, you may "opam upgrade" these packages explicitly, which will ask permission to downgrade or uninstall the conflicting packages.
Nothing to do.
22:00:06 coqgym #=# git clone https://github.com/princeton-vl/CoqGym
Cloning into 'CoqGym'...
remote: Enumerating objects: 4, done.
remote: Counting objects: 100% (4/4), done.
remote: Compressing objects: 100% (4/4), done.
remote: Total 11740 (delta 0), reused 0 (delta 0), pack-reused 11736
Receiving objects: 100% (11740/11740), 32.70 MiB | 11.09 MiB/s, done.
Resolving deltas: 100% (1683/1683), done.
Updating files: 100% (11496/11496), done.
22:00:28 coqgym #=# cd CoqGym && source install.sh
Installing Dependencies..
opam: PACKAGES... arguments: Invalid character in package name "dune=1.10.0
      cmdliner=1.0.4 ppx_sexp_conv=v0.12.0 ppx_deriving=4.3 sexplib=v0.12.0
      ppx_import=1.6.2 camlp5=7.08 coq=8.9.1"
Usage: opam install [OPTION]... [PACKAGES]...
Try `opam install --help' or `opam --help' for more information.
Dependencies installed
Installing Coq..
Error: cannot find 'ocamlfind' in your path!
Please adjust your path or use the -ocamlfind option of ./configure
Configuration script failed!
Coq installed
Installing SerAPI..
dune build
make: dune: No such file or directory
make: *** [build] Error 1
install.sh:22: command not found: dune
SerAPI installed
Installing CoqHammer..
coq_makefile -f _CoqProject -o Makefile.coq
/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: No such file or directory
CAMLDEP src/provers.mli
CAMLDEP src/features.mli
CAMLDEP src/coq_transl.mli
CAMLDEP src/tptp_out.mli
CAMLDEP src/coq_convert.mli
CAMLDEP src/hashing.mli
CAMLDEP src/coq_typing.mli
CAMLDEP src/defhash.mli
COQDEP src/hammer_plugin.mllib
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
CAMLDEP src/partac.ml
CAMLDEP src/provers.ml
File "src/provers.ml", line 193, characters 143-145:
Warning 14: illegal backslash escape in string.
CAMLDEP src/features.ml
CAMLDEP src/parallel.ml
CAMLDEP src/opt.ml
CAMLDEP src/coq_transl.ml
CAMLDEP src/tptp_out.ml
CAMLDEP src/coq_convert.ml
CAMLDEP src/hashing.ml
CAMLDEP src/coq_typing.ml
CAMLDEP src/defhash.ml
CAMLDEP src/coqterms.ml
CAMLDEP src/coq_transl_opts.ml
CAMLDEP src/timeout.ml
CAMLDEP src/msg.ml
CAMLDEP src/hh_term.ml
CAMLDEP src/hhlib.ml
CAMLDEP src/hammer_errors.ml
make[1]: printconf: Command not found
CAMLDEP -pp src/hammer.ml4
sh: -I: command not found
File "src/hammer.ml4", line 1:
Error: Error while running external preprocessor
Command line:  -I  -I /grammar compat5.cmo  grammar.cma  -impl 'src/hammer.ml4' > /var/folders/bk/jzgxbvbj67x8kjdptbj814y80000gn/T/ocamlppbeacc8

COQDEP theories/Hammer.v
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
COQDEP theories/Reconstr.v
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: No such file or directory
COQDEP src/hammer_plugin.mllib
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
make[1]: printconf: Command not found
CAMLDEP -pp src/hammer.ml4
sh: -I: command not found
File "src/hammer.ml4", line 1:
Error: Error while running external preprocessor
Command line:  -I  -I /grammar compat5.cmo  grammar.cma  -impl 'src/hammer.ml4' > /var/folders/bk/jzgxbvbj67x8kjdptbj814y80000gn/T/ocamlppccf733

COQDEP theories/Hammer.v
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
COQDEP theories/Reconstr.v
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
COQC theories/Reconstr.v
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqc: No such file or directory
make[1]: *** [theories/Reconstr.vo] Error 127
make: *** [all] Error 2
/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq install
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: No such file or directory
COQDEP src/hammer_plugin.mllib
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
make[1]: printconf: Command not found
CAMLDEP -pp src/hammer.ml4
sh: -I: command not found
File "src/hammer.ml4", line 1:
Error: Error while running external preprocessor
Command line:  -I  -I /grammar compat5.cmo  grammar.cma  -impl 'src/hammer.ml4' > /var/folders/bk/jzgxbvbj67x8kjdptbj814y80000gn/T/ocamlpp430043

COQDEP theories/Hammer.v
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
COQDEP theories/Reconstr.v
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqdep: No such file or directory
make[1]: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: Command not found
make[1]: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: Command not found
make[1]: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: Command not found
make[1]: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: Command not found
cd "src" && for i in hammer_plugin.cma coq_convert.cmi coq_transl.cmi coq_transl_opts.cmi coq_typing.cmi coqterms.cmi defhash.cmi features.cmi hammer.cmi hammer_errors.cmi hashing.cmi hh_term.cmi hhlib.cmi msg.cmi opt.cmi parallel.cmi partac.cmi provers.cmi timeout.cmi tptp_out.cmi hammer.cmo hammer_errors.cmo hhlib.cmo hh_term.cmo msg.cmo timeout.cmo coq_transl_opts.cmo coqterms.cmo defhash.cmo coq_typing.cmo hashing.cmo coq_convert.cmo tptp_out.cmo coq_transl.cmo opt.cmo parallel.cmo features.cmo provers.cmo partac.cmo; do \
	 install -d "`dirname """user-contrib"/Hammer/$i`"; \
	 install -m 0644 $i """user-contrib"/Hammer/$i; \
	done
install: hammer_plugin.cma: No such file or directory
install: coq_convert.cmi: No such file or directory
install: coq_transl.cmi: No such file or directory
install: coq_transl_opts.cmi: No such file or directory
install: coq_typing.cmi: No such file or directory
install: coqterms.cmi: No such file or directory
install: defhash.cmi: No such file or directory
install: features.cmi: No such file or directory
install: hammer.cmi: No such file or directory
install: hammer_errors.cmi: No such file or directory
install: hashing.cmi: No such file or directory
install: hh_term.cmi: No such file or directory
install: hhlib.cmi: No such file or directory
install: msg.cmi: No such file or directory
install: opt.cmi: No such file or directory
install: parallel.cmi: No such file or directory
install: partac.cmi: No such file or directory
install: provers.cmi: No such file or directory
install: timeout.cmi: No such file or directory
install: tptp_out.cmi: No such file or directory
install: hammer.cmo: No such file or directory
install: hammer_errors.cmo: No such file or directory
install: hhlib.cmo: No such file or directory
install: hh_term.cmo: No such file or directory
install: msg.cmo: No such file or directory
install: timeout.cmo: No such file or directory
install: coq_transl_opts.cmo: No such file or directory
install: coqterms.cmo: No such file or directory
install: defhash.cmo: No such file or directory
install: coq_typing.cmo: No such file or directory
install: hashing.cmo: No such file or directory
install: coq_convert.cmo: No such file or directory
install: tptp_out.cmo: No such file or directory
install: coq_transl.cmo: No such file or directory
install: opt.cmo: No such file or directory
install: parallel.cmo: No such file or directory
install: features.cmo: No such file or directory
install: provers.cmo: No such file or directory
install: partac.cmo: No such file or directory
make[1]: *** [install] Error 71
make: *** [install] Error 2
CoqHammer installed
22:00:43 CoqGym #=# cd coq_projects && make && cd ..
/Library/Developer/CommandLineTools/usr/bin/make core-dependencies
/Library/Developer/CommandLineTools/usr/bin/make math-comp
cd math-comp/mathcomp/ && make && make install
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: No such file or directory
/bin/sh: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coqtop: No such file or directory
/bin/sh: line 0: [: =: unary operator expected
/Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coq_makefile  -f Make -o Makefile.coq
make[3]: /Users/boltonbailey/Documents/MyDocuments/UIUC/Classes/FourthYear/Fall/CS598YW/Project/coqgym/CoqGym/coq/bin/coq_makefile: No such file or directory
make[3]: *** [Makefile.coq] Error 1
make[2]: *** [math-comp] Error 2
make[1]: *** [core-dependencies] Error 2
make: *** [all] Error 2
22:01:02 coq_projects #=#

I am on macOS 10.15.6
@yangky11
Copy link
Collaborator

The fist error happened when calling opam install. I just updated install.sh. Could you please try again?

@yangky11 yangky11 closed this as completed Nov 2, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@yangky11 @BoltonBailey