diff --git a/.envrc b/.envrc new file mode 100644 index 00000000..3550a30f --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 79c83625..ba245c0e 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -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 @@ -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 diff --git a/.gitignore b/.gitignore index b767639e..eb2c9839 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,8 @@ _opam .git-ps *.cache + +.direnv +# Nix build will produce this +result + diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9d334298..aa1d1cf4 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -61,9 +61,13 @@ 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: @@ -71,7 +75,8 @@ 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. #### Releasing diff --git a/README.md b/README.md index 5a9bce91..1ddc97b9 100644 --- a/README.md +++ b/README.md @@ -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; }; +... +programs.vscode = { + enable = true; + extensions = with pkgs.vscode-extensions; [ + ... + inputs.coq-lsp.packages.${pkgs.system}.vscode-extension + ... + ]; +}; +``` ### FAQ diff --git a/default.nix b/default.nix index 19a8f813..c7d0c267 100644 --- a/default.nix +++ b/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 diff --git a/editor/code/flakeModule.nix b/editor/code/flakeModule.nix new file mode 100644 index 00000000..3ecea7ce --- /dev/null +++ b/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; + }; +} diff --git a/flake.lock b/flake.lock index 92194a57..3aff546d 100644 --- a/flake.lock +++ b/flake.lock @@ -1,58 +1,62 @@ { "nodes": { - "flake-compat": { + "coq-serapi": { "flake": false, "locked": { - "lastModified": 1627913399, - "narHash": "sha256-hY8g6H2KFL8ownSiFeMOjwPC8P0ueXpCVEbxgda3pko=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "12c64ca55c1014cdc1b16ed5a804aa8576601ff2", + "lastModified": 1673473454, + "narHash": "sha256-ZeKkbEcTfe/5X/pW+Kl4Xjcj3cdZcs06LTg4dZIuHq8=", + "owner": "ejgallego", + "repo": "coq-serapi", + "rev": "79880d37705b6ec08108f5e6044fd7a128923753", "type": "github" }, "original": { - "owner": "edolstra", - "repo": "flake-compat", + "owner": "ejgallego", + "ref": "v8.17", + "repo": "coq-serapi", "type": "github" } }, - "flake-utils": { + "flake-compat": { + "flake": false, "locked": { - "lastModified": 1667395993, - "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f", + "lastModified": 1673956053, + "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", "type": "github" }, "original": { - "owner": "numtide", - "repo": "flake-utils", + "owner": "edolstra", + "repo": "flake-compat", "type": "github" } }, - "flake-utils_2": { + "flake-parts": { + "inputs": { + "nixpkgs-lib": "nixpkgs-lib" + }, "locked": { - "lastModified": 1667395993, - "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f", + "lastModified": 1675933616, + "narHash": "sha256-/rczJkJHtx16IFxMmAWu5nNYcSXNg1YYXTHoGjLrLUA=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "47478a4a003e745402acf63be7f9a092d51b83d7", "type": "github" }, "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" + "id": "flake-parts", + "type": "indirect" } }, - "flake-utils_3": { + "flake-utils": { "locked": { - "lastModified": 1638122382, - "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=", + "lastModified": 1659877975, + "narHash": "sha256-zllb8aq3YO3h8B/U0/J1WBgAL8EX5yWf5pMj3G0NAmc=", "owner": "numtide", "repo": "flake-utils", - "rev": "74f7e4319258e287b0f9cb95426c9853b282730b", + "rev": "c0e246b9b83f637f4681389ecabcb2681b4f3af0", "type": "github" }, "original": { @@ -61,198 +65,118 @@ "type": "github" } }, - "mirage-opam-overlays": { - "flake": false, + "napalm": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + }, "locked": { - "lastModified": 1661959605, - "narHash": "sha256-CPTuhYML3F4J58flfp3ZbMNhkRkVFKmBEYBZY5tnQwA=", - "owner": "dune-universe", - "repo": "mirage-opam-overlays", - "rev": "05f1c1823d891ce4d8adab91f5db3ac51d86dc0b", + "lastModified": 1672245824, + "narHash": "sha256-i596lbPiA/Rfx3DiJiCluxdgxWY7oGSgYMT7OmM+zik=", + "owner": "nix-community", + "repo": "napalm", + "rev": "7c25a05cef52dc405f4688422ce0046ca94aadcf", "type": "github" }, "original": { - "owner": "dune-universe", - "repo": "mirage-opam-overlays", + "owner": "nix-community", + "repo": "napalm", "type": "github" } }, "nixpkgs": { "locked": { - "lastModified": 1672366314, - "narHash": "sha256-F/LEtdZ90LqFzLaGtUmzsJFtarFsPJzxM9rahkb24FM=", - "owner": "nixos", + "lastModified": 1663087123, + "narHash": "sha256-cNIRkF/J4mRxDtNYw+9/fBNq/NOA2nCuPOa3EdIyeDs=", + "owner": "NixOS", "repo": "nixpkgs", - "rev": "726088a96454587d4a640d28ec442126518e449b", + "rev": "9608ace7009ce5bc3aeb940095e01553e635cbc7", "type": "github" }, "original": { - "owner": "nixos", - "ref": "nixpkgs-unstable", + "owner": "NixOS", + "ref": "nixos-unstable", "repo": "nixpkgs", "type": "github" } }, - "nixpkgs_2": { + "nixpkgs-lib": { "locked": { - "lastModified": 1657802959, - "narHash": "sha256-9+JWARSdlL8KiH3ymnKDXltE1vM+/WEJ78F5B1kjXys=", - "owner": "nixos", + "dir": "lib", + "lastModified": 1675183161, + "narHash": "sha256-Zq8sNgAxDckpn7tJo7V1afRSk2eoVbu3OjI1QklGLNg=", + "owner": "NixOS", "repo": "nixpkgs", - "rev": "4a01ca36d6bfc133bc617e661916a81327c9bbc8", + "rev": "e1e1b192c1a5aab2960bf0a0bd53a2e8124fa18e", "type": "github" }, "original": { - "owner": "nixos", + "dir": "lib", + "owner": "NixOS", "ref": "nixos-unstable", "repo": "nixpkgs", "type": "github" } }, - "ocamllsp": { - "inputs": { - "flake-utils": "flake-utils_2", - "nixpkgs": [ - "nixpkgs" - ], - "opam-nix": [ - "opam-nix" - ], - "opam-repository": "opam-repository" - }, - "locked": { - "lastModified": 1672361134, - "narHash": "sha256-zXvIZfrV0/saOmG/IZbqIfC0KkdCc8kTIkLfR6KbDDc=", - "ref": "refs/heads/master", - "rev": "8367f37bab3fb036e19892e46843d3807e25b3a8", - "revCount": 1927, - "submodules": true, - "type": "git", - "url": "https://www.github.com/ocaml/ocaml-lsp" - }, - "original": { - "submodules": true, - "type": "git", - "url": "https://www.github.com/ocaml/ocaml-lsp" - } - }, - "opam-nix": { - "inputs": { - "flake-compat": "flake-compat", - "flake-utils": "flake-utils_3", - "mirage-opam-overlays": "mirage-opam-overlays", - "nixpkgs": "nixpkgs_2", - "opam-overlays": "opam-overlays", - "opam-repository": "opam-repository_2", - "opam2json": "opam2json" - }, - "locked": { - "lastModified": 1670004517, - "narHash": "sha256-7SffiN2S9pVfOoBCcEdY/iJe28p/eiRqVLXG7/8Jb3I=", - "owner": "tweag", - "repo": "opam-nix", - "rev": "b12b7fcd6f9ea0a8a939c05c68a95525f0d80af6", - "type": "github" - }, - "original": { - "owner": "tweag", - "repo": "opam-nix", - "type": "github" - } - }, - "opam-overlays": { - "flake": false, - "locked": { - "lastModified": 1654162756, - "narHash": "sha256-RV68fUK+O3zTx61iiHIoS0LvIk0E4voMp+0SwRg6G6c=", - "owner": "dune-universe", - "repo": "opam-overlays", - "rev": "c8f6ef0fc5272f254df4a971a47de7848cc1c8a4", - "type": "github" - }, - "original": { - "owner": "dune-universe", - "repo": "opam-overlays", - "type": "github" - } - }, - "opam-repository": { - "flake": false, + "nixpkgs_2": { "locked": { - "lastModified": 1671196811, - "narHash": "sha256-8mYe1yUaKpExjyGUh3ppJ2U0BRbkS1kySMoM619In4I=", - "owner": "ocaml", - "repo": "opam-repository", - "rev": "2b84338837f46d5559e476c3766ebc61ed2849f3", + "lastModified": 1675763311, + "narHash": "sha256-bz0Q2H3mxsF1CUfk26Sl9Uzi8/HFjGFD/moZHz1HebU=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "fab09085df1b60d6a0870c8a89ce26d5a4a708c2", "type": "github" }, "original": { - "owner": "ocaml", - "repo": "opam-repository", + "owner": "NixOS", + "ref": "nixos-unstable", + "repo": "nixpkgs", "type": "github" } }, - "opam-repository_2": { - "flake": false, + "nixpkgs_3": { "locked": { - "lastModified": 1661161626, - "narHash": "sha256-J3P+mXLwE2oEKTlMnx8sYRxwD/uNGSKM0AkAB7BNTxA=", - "owner": "ocaml", - "repo": "opam-repository", - "rev": "54e69ff0949a3aaec0d5e3d67898bb7f279ab09f", + "lastModified": 1675545634, + "narHash": "sha256-TbQeQcM5TA/wIho6xtzG+inUfiGzUXi8ewwttiQWYJE=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "0591d6b57bfeb55dfeec99a671843337bc2c3323", "type": "github" }, "original": { - "owner": "ocaml", - "repo": "opam-repository", + "owner": "nixos", + "ref": "nixos-unstable", + "repo": "nixpkgs", "type": "github" } }, - "opam-repository_3": { - "flake": false, - "locked": { - "lastModified": 1672313305, - "narHash": "sha256-FfmBJNaSgU2VnwHKE0rdWG47qNNjK3TQRhPovPGzRnI=", - "owner": "ocaml", - "repo": "opam-repository", - "rev": "9af04a84c30c4ddd01244cc07d626d8c1837d2c7", - "type": "github" - }, - "original": { - "owner": "ocaml", - "repo": "opam-repository", - "type": "github" + "root": { + "inputs": { + "coq-serapi": "coq-serapi", + "flake-compat": "flake-compat", + "flake-parts": "flake-parts", + "napalm": "napalm", + "nixpkgs": "nixpkgs_2", + "treefmt": "treefmt" } }, - "opam2json": { + "treefmt": { "inputs": { - "nixpkgs": [ - "opam-nix", - "nixpkgs" - ] + "nixpkgs": "nixpkgs_3" }, "locked": { - "lastModified": 1665671715, - "narHash": "sha256-7f75C6fIkiLzfkwLpJxlQIKf+YORGsXGV8Dr2LDDi+A=", - "owner": "tweag", - "repo": "opam2json", - "rev": "32fa2dcd993a27f9e75ee46fb8b78a7cd5d05113", + "lastModified": 1675939481, + "narHash": "sha256-LwwcWeyExA02GGn8QCQfZjft+blg101OXBQWglCqPVA=", + "owner": "numtide", + "repo": "treefmt-nix", + "rev": "e9033eca3d7139fd499f310023ddc3bb5abff515", "type": "github" }, "original": { - "owner": "tweag", - "repo": "opam2json", + "owner": "numtide", + "repo": "treefmt-nix", "type": "github" } - }, - "root": { - "inputs": { - "flake-utils": "flake-utils", - "nixpkgs": "nixpkgs", - "ocamllsp": "ocamllsp", - "opam-nix": "opam-nix", - "opam-repository": "opam-repository_3" - } } }, "root": "root", diff --git a/flake.nix b/flake.nix index ee6bbe62..16d0af51 100644 --- a/flake.nix +++ b/flake.nix @@ -1,70 +1,98 @@ { - inputs = { - nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; - opam-nix.url = "github:tweag/opam-nix"; - flake-utils.url = "github:numtide/flake-utils"; - ocamllsp.url = "git+https://www.github.com/ocaml/ocaml-lsp?submodules=1"; - ocamllsp.inputs.opam-nix.follows = "opam-nix"; - ocamllsp.inputs.nixpkgs.follows = "nixpkgs"; - opam-repository = { - url = "github:ocaml/opam-repository"; - flake = false; - }; - }; - outputs = { self, flake-utils, opam-nix, nixpkgs, ocamllsp, opam-repository }@inputs: - let package = "coq-lsp"; - in flake-utils.lib.eachDefaultSystem (system: - let - devPackages = { - # Extra packages for testing - }; - pkgs = nixpkgs.legacyPackages.${system}; - ocamlformat = - # Detection of ocamlformat version from .ocamlformat file - let - ocamlformat_version = - let - lists = pkgs.lib.lists; - strings = pkgs.lib.strings; - ocamlformat_config = strings.splitString "\n" (builtins.readFile ./.ocamlformat); - prefix = "version="; - ocamlformat_version_pred = line: strings.hasPrefix prefix line; - version_line = lists.findFirst ocamlformat_version_pred "not_found" ocamlformat_config; - version = strings.removePrefix prefix version_line; - in - builtins.replaceStrings [ "." ] [ "_" ] version; - in - builtins.getAttr ("ocamlformat_" + ocamlformat_version) pkgs; - in - { - packages = - let - scope = opam-nix.lib.${system}.buildOpamProject' - { - repos = [ opam-repository ]; - } ./. - (devPackages // { ocaml-base-compiler = "4.14.0"; }); + description = "A language server (LSP) for the Coq theorem prover"; + + outputs = inputs @ { + self, + flake-parts, + treefmt, + ... + }: + flake-parts.lib.mkFlake {inherit inputs;} { + systems = ["x86_64-linux" "aarch64-linux" "x86_64-darwin" "aarch64-darwin"]; + imports = [treefmt.flakeModule ./editor/code/flakeModule.nix]; + + perSystem = { + config, + pkgs, + lib, + ... + }: let + l = lib // builtins; + coq_8_17 = pkgs.coqPackages_8_17; + coqPackages = coq_8_17.coqPackages; + ocamlPackages = coq_8_17.coq.ocamlPackages; + in { + packages.default = config.packages.coq-lsp; + + # NOTE(2023-06-02): Nix does not support top-level self submodules (yet) + packages.coq-lsp = ocamlPackages.buildDunePackage { + duneVersion = "3"; + + pname = "coq-lsp"; + version = "${self.lastModifiedDate}+8.17-rc1"; + + src = self.outPath; + + nativeBuildInputs = l.attrValues { + inherit (ocamlPackages) menhir; + }; + + propagatedBuildInputs = let + serapi = + (coqPackages.lib.overrideCoqDerivation { + defaultVersion = "8.17.0+0.17.0"; + } + coqPackages.serapi) + .overrideAttrs (_: { + src = inputs.coq-serapi; + }); in - scope // { default = self.packages.${system}.${package}; }; + l.attrValues { + inherit serapi; + inherit (ocamlPackages) yojson cmdliner uri; + }; + }; + + treefmt.config = { + projectRootFile = "dune-project"; - devShells.fmt = - pkgs.mkShell { - inputsFrom = [ pkgs.dune_3 ]; - buildInputs = [ pkgs.dune_3 ocamlformat ]; + flakeFormatter = true; + + settings.global.excludes = ["./vendor/**"]; + + programs.alejandra.enable = true; + programs.ocamlformat = { + enable = true; + configFile = ./.ocamlformat; }; + }; + + devShells.default = pkgs.mkShell { + inputsFrom = [config.packages.coq-lsp]; - devShell = - pkgs.mkShell { - nativeBuildInputs = [ pkgs.opam ]; - buildInputs = (with pkgs; - [ - # dev tools - ocamlformat - nodejs - ]) ++ [ ocamllsp.outputs.packages.${system}.ocaml-lsp-server ] - ++ (builtins.map (s: builtins.getAttr s self.packages.${system}) - (builtins.attrNames devPackages)); - inputsFrom = [ self.packages.${system}.default ]; + packages = l.attrValues { + inherit (config.treefmt.build) wrapper; + inherit (pkgs) dune_3; + inherit (ocamlPackages) ocaml ocaml-lsp; }; - }); + }; + }; + }; + + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; + treefmt.url = "github:numtide/treefmt-nix"; + + napalm.url = "github:nix-community/napalm"; + + flake-compat = { + url = "github:edolstra/flake-compat"; + flake = false; + }; + + coq-serapi = { + url = "github:ejgallego/coq-serapi/v8.17"; + flake = false; + }; + }; } diff --git a/shell.nix b/shell.nix new file mode 100644 index 00000000..e6d91731 --- /dev/null +++ b/shell.nix @@ -0,0 +1,14 @@ +( + 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 = ./.;} +) +.shellNix