CertiCoq 0.9 ExtLib upper bound #2894
Conversation
| @@ -27,11 +27,12 @@ install: [ | |||
| ] | |||
| depends: [ | |||
| "ocaml" | |||
| "conf-clang" | |||
There was a problem hiding this comment.
| "conf-clang" | |
| ("conf-clang" | "conf-gcc") |
It seems unlikely that CertiCoq is tied to Clang specifically, rather than just "any" C compiler. The suggestion is the current best approximation in opam of how to depend on any C compiler.
There was a problem hiding this comment.
Clang only: CertiCoq/certicoq#62
There was a problem hiding this comment.
gcc is painfully slow on large examples, but can be used sometimes. Also the compcert compiler can be used. For now clang is the safest bet.
There was a problem hiding this comment.
Last time I checked, you were compiling with -O0. In the case of GCC, this is a bad idea because the non-optimized generated code ends up being so large that it bring the compiler backend to its knees. GCC is often faster when using -O1 (not counting the huge benefit for the compiled program).
There was a problem hiding this comment.
What's the status of this thread? I can see two directions:
- Test
gcc -O1. If it works fine, then allow either Clang or GCC as dependency; or - Stick to Clang, and install it in the CI environment.
There was a problem hiding this comment.
Maybe @mattam82 can make the call? You can add Clang into the CI environment by modifying .gitlab-ci.yml.
No description provided.