Stream: coq-lsp

Topic: Nix Setup


view this post on Zulip r-muhairi (Feb 06 2023 at 07:06):

side question

@Emilio Jesús Gallego Arias do you use nix flakes or do you still use nix channels?

I opened https://github.com/ejgallego/coq-lsp/pull/284 however I didn't document anything related to nix-channels and replaced the previous outdated default.nix with compat that probably doesn't work as there's no way to explicitly pass in submodules, well outside of course just cloning the project with submodules in the first place (should work then).

p.s the previous flake didn't build and the default.nix seemed to have been outdated

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 09:04):

Hi @r-muhairi , @Ali Caglayan knows about the Nix setup, thanks a lot for the PR.

view this post on Zulip Notification Bot (Feb 06 2023 at 09:04):

2 messages were moved here from #coq-lsp > General Chat by Emilio Jesús Gallego Arias.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 06 2023 at 09:05):

I'm very happy with whatever setup is best for Nix, I myself don't use Nix yet (opam is very convenient for certain OCaml workflows)

view this post on Zulip r-muhairi (Feb 06 2023 at 09:07):

Emilio Jesús Gallego Arias said:

I'm very happy with whatever setup is best for Nix, I myself don't use Nix yet (opam is very convenient for certain OCaml workflows)

Oh you weren't a nix user? My bad, I made an assumption based on the mention of nix in the Serapi README

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:03):

I am using flakes. You need to do nix develop in the repo. And there is a way to pull submodules, have a look at CONTRIBUTING.

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:04):

Default.nix is out of date however

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:07):

So things like nix build .?submodules=1 work

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:07):

You also do the same submodules trick in the URL for other flake inputs

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:07):

The only issue is that there is no good way to keep the submodule coq and whatever coq you are using the same atm.

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:08):

So if anybody can write a flake without submodules that would be cool.

view this post on Zulip r-muhairi (Feb 06 2023 at 10:09):

Ali Caglayan said:

The only issue is that there is no good way to keep the submodule coq and whatever coq you are using the same atm.

That's where your mistaken, i'm not pinning coq as a flake input nor mentioning it anywhere in the flake
dune vendors it for me

only thing actually added as an input is coq-serapi

view this post on Zulip r-muhairi (Feb 06 2023 at 10:11):

you do need the submodules to develop anyhow so i presume any developer would just clone/initwith submodules

on nix build just asking to pass ?submodules=1 shouldn't be that problematic

view this post on Zulip r-muhairi (Feb 06 2023 at 10:13):

Ali Caglayan said:

So if anybody can write a flake without submodules that would be cool.

the submodules are apart of the project they're necessary for building, you could have a makeshift situation where you vendor them manually with nix however that would be unnecessary and redundant

view this post on Zulip r-muhairi (Feb 06 2023 at 10:32):

@Ali Caglayan ocaml-lsp is there, i don't know why there was a ocamlformat detection in the first place

view this post on Zulip r-muhairi (Feb 06 2023 at 10:33):

i asked rgrinberg the same question

here is what i asked him exactly

Is there any reason why you'd use a different nixpkgs version of ocamlformat?
If you wanted to lock the default profile at a specific version does newer versions of ocamlformat not support previous versions defined in .ocamlformat?

he hasn't responded yet.

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:34):

Well each version of ocaml format makes some formatting changes so it's best to stick to the one in the OCaml format file.

view this post on Zulip r-muhairi (Feb 06 2023 at 10:35):

yeah but you can restrict the version in the ocamlformat file no?

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:35):

The code in the flake reads the file and pulls that one from nixpkgs

view this post on Zulip r-muhairi (Feb 06 2023 at 10:35):

do read this, https://github.com/ocaml-ppx/ocamlformat#-usage
there is a version option

view this post on Zulip Ali Caglayan (Feb 06 2023 at 10:35):

It's Rudis code originally btw

view this post on Zulip r-muhairi (Feb 06 2023 at 10:38):

in regards to the CONTRIBUTING.md, I guess I can remove the in this repository part of the nix README modification i added

view this post on Zulip r-muhairi (Feb 06 2023 at 10:39):

the instructions still apply as long as they clone with submodules btw

however i did introduce a new devShell for the vscode client if you want to document that as well? I don't personally think its necessary

edit: pushed documentation for it anyhow alongside the vscode-extension instructions

view this post on Zulip r-muhairi (Feb 06 2023 at 11:29):

@Ali Caglayan I see why the detection was there in the first place

image.png

view this post on Zulip r-muhairi (Feb 06 2023 at 11:30):

however there's no need for the detection in this flake, i'll push something up too treefmt-nix in the ocamlformat nix module

view this post on Zulip r-muhairi (Feb 06 2023 at 12:42):

https://github.com/numtide/treefmt-nix/pull/41/files
once it is merged we can just pass ./.ocamlformat to the package option

view this post on Zulip r-muhairi (Feb 06 2023 at 15:34):

@Ali Caglayan https://github.com/numtide/treefmt-nix/issues/42
manually setting each exclude for the formatters works but its fine just to wait for the issue to resolve as to also get the other PR for extracting the version merged alongside it

view this post on Zulip r-muhairi (Feb 08 2023 at 09:00):

@Ali Caglayan I excluded the vendor directory from formatting as the treefmt PR for that went through, however for the version detection, not yet, not sure if it will, so i just added a modified version in the last commit.

its merge-able if everything is ok

view this post on Zulip Ali Caglayan (Feb 08 2023 at 14:18):

OK, I will test it out later

view this post on Zulip r-muhairi (Feb 09 2023 at 19:12):

@Ali Caglayan rebased, got it building with the latest deps (menhir, uri)

view this post on Zulip Ali Caglayan (Feb 09 2023 at 19:14):

I'll check it out later

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 14:41):

Hi folks, I had some reports that coq-lsp under Nix was not in the right version for 8.18 , is there an easy way to check what is going on here?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2023 at 14:41):

I still know 0 about Nix but I'm trying to learn and ensure things are friendly for Nix users.


Last updated: Mar 28 2024 at 23:01 UTC