UniMath / Schools

77 stars 21 forks source link

Error when running make file; probably Schools points to old version of Coq? #46

Open paigenorth opened 3 years ago

paigenorth commented 3 years ago

Last bit of terminal output:

clang: warning: optimization flag '-fexcess-precision=standard' is not supported [-Wignored-optimization-argument] OCAMLC kernel/byterun/coq_memory.c clang: warning: optimization flag '-fexcess-precision=standard' is not supported [-Wignored-optimization-argument] OCAMLC kernel/byterun/coq_values.c clang: warning: optimization flag '-fexcess-precision=standard' is not supported [-Wignored-optimization-argument] OCAMLC kernel/byterun/coq_interp.c clang: warning: optimization flag '-fexcess-precision=standard' is not supported [-Wignored-optimization-argument] cd kernel/byterun/ && \ "/usr/local/bin/ocamlfind" ocamlmklib -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o COQMKTOP -o bin/coqtop.opt Undefined symbols for architecture x86_64: "_caml_young_limit", referenced from: _coq_interprete in libcoqrun.a(coq_interp.o) "_caml_young_ptr", referenced from: _coq_interprete in libcoqrun.a(coq_interp.o) ld: symbol(s) not found for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) File "caml_startup", line 1: Error: Error during linking (exit code 1) make[3]: [bin/coqtop.opt] Error 2 make[3]: Leaving directory `/Users/joegould/Documents/Schools/UniMath/sub/coq' make[2]: [submake] Error 2 make[2]: Leaving directory `/Users/joegould/Documents/Schools/UniMath/sub/coq' make[1]: [sub/coq/bin/coq_makefile] Error 2 make: [build_UniMath] Error 2

benediktahrens commented 3 years ago

Not sure where this error comes from.

In any case, I have just updated the UniMath submodule to the latest version - would you mind trying again?