Unverified Commit 99f9f572 authored by Théo Zimmermann's avatar Théo Zimmermann Committed by GitHub
Browse files

vscoq -> 2.3.0 & add vsrocq extension (#460186)

parents 1992c4c4 72f6c87a
Loading
Loading
Loading
Loading
+16 −0
Original line number Diff line number Diff line
@@ -3933,6 +3933,22 @@ let

      robocorp.robotframework-lsp = callPackage ./robocorp.robotframework-lsp { };

      rocq-prover.vsrocq = buildVscodeMarketplaceExtension {
        mktplcRef = {
          publisher = "rocq-prover";
          name = "vsrocq";
          version = "2.3.2";
          hash = "sha256-S3rKCzdGb5/UAJC6Z5GGC1Brib9PKiqQv8dRANYbp70=";
        };
        meta = {
          description = "VsRocq is an extension for Visual Studio Code with support for the Rocq Prover";
          downloadPage = "https://marketplace.visualstudio.com/items?itemName=rocq-prover.vsrocq";
          homepage = "https://github.com/rocq-prover/vsrocq";
          license = lib.licenses.mit;
          maintainers = [ lib.maintainers.Zimmi48 ];
        };
      };

      roman.ayu-next = buildVscodeMarketplaceExtension {
        mktplcRef = {
          name = "ayu-next";
+3 −0
Original line number Diff line number Diff line
@@ -16,6 +16,7 @@ let
    in
    with lib.versions;
    lib.switch coq.coq-version [
      (case (range "8.18" "9.1") "2.3.3")
      (case (range "8.18" "9.1") "2.2.6")
      (case (range "8.18" "8.20") "2.2.1")
      (case (range "8.18" "8.19") "2.1.2")
@@ -41,6 +42,8 @@ let
    release."2.2.5".sha256 = "sha256-XyIjwem/yS7UIpQATNixgKkrMOHHs74nkAOvpU5WG1k=";
    release."2.2.6".rev = "v2.2.6";
    release."2.2.6".sha256 = "sha256-J8nRTAwN6GBEYgqlXa2kkkrHPatXsSObQg9QUQoZhgE=";
    release."2.3.3".rev = "v2.3.3";
    release."2.3.3".sha256 = "sha256-wgn28wqWhZS4UOLUblkgXQISgLV+XdSIIEMx9uMT/ig=";
    inherit location;
  };
  fetched = fetch (if version != null then version else defaultVersion);
+80 −0
Original line number Diff line number Diff line
{
  metaFetch,
  coq,
  rocq-core,
  lib,
  glib,
  adwaita-icon-theme,
  wrapGAppsHook3,
  version ? null,
}:

let
  ocamlPackages = rocq-core.ocamlPackages;
  defaultVersion =
    let
      case = case: out: { inherit case out; };
    in
    with lib.versions;
    lib.switch rocq-core.rocq-version [
      (case (range "8.18" "9.1") "2.3.3")
      (case (range "8.18" "9.1") "2.3.0")
    ] null;
  location = {
    domain = "github.com";
    owner = "rocq-prover";
    repo = "vsrocq";
  };
  fetch = metaFetch {
    release."2.3.0".rev = "v2.3.0";
    release."2.3.0".sha256 = "sha256-BZLxcCmSGFf04eUmlJXnyxmg4hTwpFaPaIik4VD444M=";
    release."2.3.3".rev = "v2.3.3";
    release."2.3.3".sha256 = "sha256-wgn28wqWhZS4UOLUblkgXQISgLV+XdSIIEMx9uMT/ig=";
    inherit location;
  };
  fetched = fetch (if version != null then version else defaultVersion);
in
ocamlPackages.buildDunePackage {
  pname = "vsrocq-language-server";
  inherit (fetched) version;
  src = "${fetched.src}/language-server";
  nativeBuildInputs = [ coq ];
  buildInputs = [
    coq
    glib
    adwaita-icon-theme
    wrapGAppsHook3
  ]
  ++ (with ocamlPackages; [
    findlib
    lablgtk3-sourceview3
    yojson
    zarith
    ppx_inline_test
    ppx_assert
    ppx_sexp_conv
    ppx_deriving
    ppx_import
    sexplib
    ppx_yojson_conv
    lsp
    sel
    ppx_optcomp
  ]);
  preBuild = ''
    make dune-files
  '';

  meta =
    with lib;
    {
      description = "Language server for the vsrocq vscode/codium extension";
      homepage = "https://github.com/rocq-prover/vsrocq";
      maintainers = with maintainers; [ cohencyril ];
      license = licenses.mit;
    }
    // optionalAttrs (fetched.broken or false) {
      rocqFilter = true;
      broken = true;
    };
}
+1 −0
Original line number Diff line number Diff line
@@ -40,6 +40,7 @@ let
      parseque = callPackage ../development/rocq-modules/parseque { };
      rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
      stdlib = callPackage ../development/rocq-modules/stdlib { };
      vsrocq-language-server = callPackage ../development/rocq-modules/vsrocq-language-server { };

      filterPackages = doesFilter: if doesFilter then filterRocqPackages self else self;
    };