search

tydeu / lean4-alloy

Write C shims from within Lean code.
Apache License 2.0
42 stars 11 forks source link

feat: Add nix flake build #1

Closed Anderssorby closed 8 months ago

Anderssorby commented 1 year ago

This adds a nix flake build and updates the lean support to the most recent version.

I also suggest renaming the project to Alloy.lean.

tydeu commented 1 year ago

I like the current project name, why change it? It also better indicates that the project is for Lean 4 (and not Lean 3).

Regardless, I did make the necessary changes to update the project to the Lean 05-20 nightly. There were some slight differences in the way I did it (plus I also updated the example), so please rebase upon them.

On the main point, the addition of a nix flake build looks fine. However, I don't understand why you have added an essentially empty tests directory or why you need to add *.olean to the .gitignore? What is sticking oleans out in the open? You didn't need to add either to the flake build you added to Lake, so I am confused why they are here. Furthermore, the flake.lock was added to the .gitignore there, but not here, which is also confusing. Similarly, it would be nice if you could model the section you added to the README on building with Nix Flakes after the same section in the Lake README.

Hopefully, I don't sound to critical. I am thankful for your interest in Alloy and would be happy to merge in a flake configuration when you pare the PR down to just that. :)

tydeu commented 9 months ago

As this PR is old and stale, I am planning on closing it soon. Any objections?