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

CertiCoq 0.9 ExtLib upper bound #2894

Merged
merged 3 commits into from
Feb 23, 2024
Merged

CertiCoq 0.9 ExtLib upper bound #2894

Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
46ff95a
CertiCoq 0.9 ExtLib upper bound
liyishuai Jan 11, 2024
b6f08c8
CertiCoq: requires Clang
liyishuai Jan 12, 2024
4d26f6d
CI: install Clang
liyishuai Feb 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion released/packages/coq-certicoq/coq-certicoq.0.9~beta+8.14/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,11 +27,12 @@ install: [
]
depends: [
"ocaml"
"conf-clang"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
"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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Clang only: CertiCoq/certicoq#62

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the status of this thread? I can see two directions:

  1. Test gcc -O1. If it works fine, then allow either Clang or GCC as dependency; or
  2. Stick to Clang, and install it in the CI environment.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe @mattam82 can make the call? You can add Clang into the CI environment by modifying .gitlab-ci.yml.

"coq" {>= "8.14" & < "8.15~"}
"coq-compcert" {= "3.11"}
"coq-equations" {= "1.3+8.14"}
"coq-metacoq-erasure" {>= "1.1.1+8.14" }
"coq-ext-lib" {>= "0.11.5"}
"coq-ext-lib" {>= "0.11.5" < "0.12.1"}
]

synopsis: "A Verified Compiler for Gallina, Written in Gallina "
Expand Down
Loading