Skip to content

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

Description

@paigenorth

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions