[flake]: Introduce flake-parts, treefmt, and other changes #284
Conversation
This comment was marked as outdated.
This comment was marked as outdated.
|
Hmm it seems you got rid of the OCaml format detection and also ocaml lsp. Can you add those back in? Also see the doc on Nix in contributing. It used to be in the readme but it was moved. |
|
We should not be formatting the submodules. Can you ignore them? |
| This currently only applies to building the default package (coq-lsp), which is the server. | ||
| Clients don't have specific submodules as of yet. |
There was a problem hiding this comment.
Rather than submodules, I would say shells. I mainly wanted the flake for development however if we wish to distribute OCaml pacakges relying on Coq libraries the situation is a bit complicated. We also want people to be able to override the serapi and coq dependencies and avoid using submodules. This is not easy to do from what I have tried.
There was a problem hiding this comment.
I don't believe submodules and shells are referring to the same thing here?
We also want people to be able to override the serapi and coq dependencies and avoid using submodules. This is not easy to do from what I have tried.
I couldn't even get it to build without coq vendored in with submodules, overriding serapi worked fine, but coq wasn't even building.
| - **Coq Platform** (coming soon) | ||
| - [Do it yourself!](#server-1) | ||
|
|
||
| #### **Visual Studio Code**: | ||
| - Official Marketplace: https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp | ||
| - Open VSX: https://open-vsx.org/extension/ejgallego/coq-lsp | ||
| - Nix: | ||
| ```nix | ||
| inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; }; |
There was a problem hiding this comment.
Why do you prefer the full url over the github: ones?
There was a problem hiding this comment.
Passing in ?submodules=1 or ?submodules=true with github: failed in my case,
|
Hello! I tested this on aarch64-darwin. I'm able to build and run the |
…ke-utils with flake-parts, use treefmt
…uilding in the repository
… client devShells
Co-authored-by: Ali Caglayan <alizter@gmail.com>
Co-authored-by: Ali Caglayan <alizter@gmail.com>
| - run: npm ci | ||
| - run: npx prettier -c . | ||
| - name: 📐 Format with alejandra, ocamlformat, prettier | ||
| run: nix fmt |
There was a problem hiding this comment.
This formats the code, I was supposed to use the check output target as opposed to running the formatter.
Tested on
x86_64-linuxNote
There's no support for enabling submodules for flake top-level yet, as such
coq-sarpiflake input needs to reflect the .gitmodule