Skip to content
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

Merged
merged 15 commits into from Feb 14, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions .envrc
@@ -0,0 +1 @@
use flake
24 changes: 4 additions & 20 deletions .github/workflows/build.yml
Expand Up @@ -88,8 +88,8 @@ jobs:
- run: npm ci
- run: npx --yes vsce ls

fmt-ocamlfmt:
name: Format with ocamlfmt
treefmt:
name: Format
runs-on: ubuntu-latest
steps:
- name: 🔭 Checkout code
Expand All @@ -98,21 +98,5 @@ jobs:
submodules: recursive
- name: ❄️ Setup Nix
uses: cachix/install-nix-action@v18
- name: 📐 Format with ocamlfmt
run: nix develop .#fmt -c make fmt

fmt-prettier:
name: Format with prettier
runs-on: ubuntu-latest
defaults:
run:
working-directory: ./editor/code
steps:
- name: 🔭 Checkout code
uses: actions/checkout@v3
- name: 🚀 Setup node
uses: actions/setup-node@v3
with:
node-version: 16
- run: npm ci
- run: npx prettier -c .
- name: 📐 Format with alejandra, ocamlformat, prettier
run: nix fmt
Copy link
Owner

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

Copy link
Contributor Author

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.

5 changes: 5 additions & 0 deletions .gitignore
Expand Up @@ -5,3 +5,8 @@ _opam
.git-ps

*.cache

.direnv
# Nix build will produce this
result
huwaireb marked this conversation as resolved.
Show resolved Hide resolved

11 changes: 8 additions & 3 deletions CONTRIBUTING.md
Expand Up @@ -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
Copy link
Collaborator

Choose a reason for hiding this comment

The 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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The 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?

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.


#### Releasing

Expand Down
22 changes: 21 additions & 1 deletion README.md
Expand Up @@ -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; };
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do you prefer the full url over the github: ones?

Copy link
Contributor Author

@huwaireb huwaireb Feb 8, 2023

Choose a reason for hiding this comment

The 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

Expand Down
39 changes: 14 additions & 25 deletions default.nix
@@ -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
52 changes: 52 additions & 0 deletions editor/code/flakeModule.nix
@@ -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;
};
}