coq / vscoq

Visual Studio Code extension for Coq
MIT License
336 stars 68 forks source link

Fix issue with build using flake system in issue #747 #754

Closed redanaheim closed 6 months ago

redanaheim commented 7 months ago

See issue #747

Overview of changes:

One possible problem: I changed the commit the coq-master dependency is derived from, which (according to the comment) may break something in the CI workflow. I'm not sure what the pinned version is, but the latest commits on coq/coq don't build with the flake system.

These changes were tested on aarch64-darwin (MacOS 14.1, nix 2.20.3) and aarch64-linux (nixOS, nix 2.18.1).

gares commented 7 months ago

Added yarn.nix files generated using yarn2nix that allow building the yarn dependencies using nix

Thanks!

Is there a way to run this tool in CI and check that the .nix is up to date wrt the yarn one? I'm not a nix user, neither is Romain AFAIK, so CI better be rock solid on nix, or we won't notice these issues timely.

redanaheim commented 7 months ago

Is there a way to run this tool in CI and check that the .nix is up to date wrt the yarn one?

Yeah, using the following command will just create a file called new_yarn.nix using the yarn.lock in the current directory (assuming nix is available at the relevant point in CI):

nix-shell -p yarn2nix --run "yarn2nix > new_yarn.nix"

Then, you could compare hashes with the committed file (yarn.nix) and error if they're not the same.

Alternatively, you could overwrite the yarn.nix with that same command, which would produce an error when building the flake because flake.lock would be out of date if the contents of yarn.nix aren't the same. That said, I'm not sure if the flake is actually built in the CI. It seems like only nix develop is used.

rtetley commented 7 months ago

Took the liberty of attempting a fix

rtetley commented 7 months ago

Argh, fixed the wrong file... Also realised retrospectively that it would have been more polite to ask for permission before pushing to the main branch of your fork. Would you mind if I push the fix on the right file @redanaheim ?

redanaheim commented 7 months ago

@rtetley No yeah it's fine go ahead, I didn't even know you could do that lol

rtetley commented 7 months ago

Haha yeah, you can opt out of it when you create the PR afaik

redanaheim commented 7 months ago

@rtetley @gares do you want me to try to implement the CI check for whether each yarn.nix is up to date? I'm thinking

nix-shell -p yarn2nix --run "yarn2nix > new_yarn.nix"
diff --brief new_yarn.nix yarn.nix

run in each directory with a yarn.nix.

rtetley commented 7 months ago

@redanaheim sounds good ! Please do :-) I'm really not that much of a nix expert...

rtetley commented 7 months ago

Okay finally looks like this should work. One little nitpick: the PIN_COQ needs to track the master branch of coq, it allows for coq developers to do PRs which keep the language server up to date with the latest coq api. What is the issue with the old pin ? It was probably currently not up to date.

redanaheim commented 7 months ago

What is the issue with the old pin ? It was probably currently not up to date.

@rtetley There is no issue, I changed it on my own fork to be the latest version that builds with flakes. I can revert it back to the version currently on main if you'd like.

rtetley commented 7 months ago

What is the issue with the old pin ? It was probably currently not up to date.

@rtetley There is no issue, I changed it on my own fork to be the latest version that builds with flakes. I can revert it back to the version currently on main if you'd like.

Ah okay cool ! Nah that sounds fine ! Thanks !