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.

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

Test Lean/Coq output when it's all working #744

Open
Timmmm opened this issue Feb 17, 2025 · 3 comments
Open

Test Lean/Coq output when it's all working #744

Timmmm opened this issue Feb 17, 2025 · 3 comments

Comments

@Timmmm
Copy link
Collaborator

Timmmm commented Feb 17, 2025

When the next Sail compiler is released we should update to it and add the Lean output to CI, and ideally Coq too if it works.

Bonus points if we can actually compile/test the Lean/Coq code somehow.

@jordancarlin
Copy link
Collaborator

Related to this, it’s probably worth testing compiling the model against the latest head of the sail compiler. Not sure whether we should do that in this repo or over in the sail repo as both potentially need changes as either evolves.

@Timmmm
Copy link
Collaborator Author

Timmmm commented Feb 17, 2025

I dunno, that means we'd have to deal with OCaml again... I'd rather just have more regular releases of the Sail compiler.

@jordancarlin
Copy link
Collaborator

We might need to deal with opam in CI again anyway if we want to actually compile alternative outputs like Coq.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants