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
[flake]: Introduce flake-parts, treefmt, and other changes #284
Changes from all commits
912d0ec
9983476
d214412
3a1210d
36abc9a
977f57a
a12a650
e4d81e7
29e1ef2
111cdf5
4063b2f
238a297
0eb6a02
5d42889
c873bf3
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
use flake |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -61,17 +61,22 @@ You can also use the regular `dune build @check` etc... targets. | |
|
||
#### Nix | ||
|
||
We have a Nix flake that you can use. For development, simply run `nix develop`. | ||
We have a Nix flake that you can use. For development, in the case of the server, simply run `nix develop`. | ||
In the case of the client, we expose separate shells, e.g client-vscode, would be `nix develop .#client-vscode` (this can be done on top of the original `nix develop`) | ||
|
||
If you wish to do `nix build` or compose this flake from another project, you | ||
You can view the list of packages and devShells that are exposed | ||
by running `nix flake show`. | ||
|
||
If you wish to do `nix build`, you | ||
will need to use the .?submodules=1` trick, since we use submodules here for | ||
vendoring. For example, building requires: | ||
|
||
``` | ||
nix build .?submodules=1 | ||
``` | ||
|
||
You can use this flake in other flakes or Nix derivations. | ||
This currently only applies to building the default package (coq-lsp), which is the server. | ||
Clients don't have specific submodules as of yet. | ||
Comment on lines
+78
to
+79
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't believe submodules and shells are referring to the same thing here?
I couldn't even get it to build without coq vendored in with submodules, overriding serapi worked fine, but coq wasn't even building. |
||
|
||
#### Releasing | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -21,13 +21,33 @@ In order to use `coq-lsp` you'll need to install [**both**](etc/FAQ.md) the | |
#### Server | ||
|
||
- **opam**: `opam install coq-lsp` | ||
- **Nix** (coming soon) | ||
- **Nix**: | ||
- In nixpkgs: [#213397](https://github.com/NixOS/nixpkgs/pull/213397) | ||
- In your flake: | ||
```nix | ||
inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; }; | ||
... | ||
coq-lsp.packages.${system}.default | ||
``` | ||
- **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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why do you prefer the full url over the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Passing in ?submodules=1 or ?submodules=true with github: failed in my case, |
||
... | ||
programs.vscode = { | ||
enable = true; | ||
extensions = with pkgs.vscode-extensions; [ | ||
... | ||
inputs.coq-lsp.packages.${pkgs.system}.vscode-extension | ||
... | ||
]; | ||
}; | ||
``` | ||
|
||
### FAQ | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,25 +1,14 @@ | ||
{ | ||
pkgs ? import (fetchTarball "https://github.com/vbgl/nixpkgs/tarball/2a4e60c330d66638897ec450126eb1e3a9a13148") {} | ||
}: | ||
|
||
with pkgs; | ||
|
||
let oc = ocaml-ng.ocamlPackages_4_07; in | ||
|
||
stdenv.mkDerivation { | ||
name = "coq-lsp-0"; | ||
src = builtins.filterSource (p: _: builtins.baseNameOf p != "_build") ./.; | ||
buildInputs = [ | ||
dune oc.ocaml oc.findlib oc.num oc.yojson oc.cmdliner | ||
oc.lablgtk | ||
]; | ||
|
||
preBuild = '' | ||
for f in kernel dev/tools | ||
do | ||
patchShebangs coq/$f | ||
done | ||
''; | ||
|
||
inherit (dune) installPhase; | ||
} | ||
( | ||
import | ||
( | ||
let | ||
lock = builtins.fromJSON (builtins.readFile ./flake.lock); | ||
in | ||
fetchTarball { | ||
url = "https://github.com/edolstra/flake-compat/archive/${lock.nodes.flake-compat.locked.rev}.tar.gz"; | ||
sha256 = lock.nodes.flake-compat.locked.narHash; | ||
} | ||
) | ||
{src = ./.;} | ||
) | ||
.defaultNix |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,52 @@ | ||
{ | ||
perSystem = { | ||
config, | ||
pkgs, | ||
lib, | ||
inputs', | ||
... | ||
}: { | ||
packages.vsix = (inputs'.napalm.legacyPackages).buildPackage ./. { | ||
installPhase = '' | ||
mkdir $out | ||
${lib.getExe pkgs.vsce} package -o $out/$name.zip > /dev/null 2>&1 | ||
''; | ||
|
||
passthru = let | ||
attrs = builtins.fromJSON (builtins.readFile ./package.json); | ||
in { | ||
extPublisher = attrs.publisher; | ||
extName = attrs.name; | ||
extVersion = attrs.version; | ||
extId = with attrs; "${publisher}.${name}"; | ||
}; | ||
}; | ||
|
||
packages.vscode-extension = let | ||
vsix = config.packages.vsix; | ||
in | ||
pkgs.vscode-utils.buildVscodeExtension | ||
{ | ||
inherit (vsix) name; | ||
|
||
version = vsix.extVersion; | ||
|
||
vscodeExtPublisher = vsix.extPublisher; | ||
vscodeExtName = vsix.extName; | ||
vscodeExtUniqueId = vsix.extId; | ||
|
||
src = "${vsix}/${vsix.name}.zip"; | ||
}; | ||
|
||
devShells.client-vscode = pkgs.mkShell { | ||
packages = builtins.attrValues { | ||
inherit (pkgs) nodejs; | ||
inherit (pkgs.nodePackages) typescript typescript-language-server; | ||
|
||
inherit (config.treefmt.build) wrapper; | ||
}; | ||
}; | ||
|
||
treefmt.config.programs.prettier.enable = true; | ||
}; | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This seems broken, see #449
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#452
This formats the code, I was supposed to use the check output target as opposed to running the formatter.