Unverified Commit 4937cffd authored by Théo Zimmermann's avatar Théo Zimmermann Committed by GitHub
Browse files

Update vsrocq (#478436)

parents 676cc199 3fafa51b

pkgs/applications/editors/vscode/extensions/default.nix

+1 −0
Original line number Diff line number Diff line
@@ -3941,6 +3941,7 @@ let 
        mktplcRef = {

          publisher = "rocq-prover";

          name = "vsrocq";

          # When updating the version here, also update the language server vsrocq-language-server

          version = "2.3.4";

          hash = "sha256-2zYoCUtyhboQt68UJEmWOvrTrIOV2QmpaXU5mUhJfsA=";

        };

pkgs/development/coq-modules/vscoq-language-server/default.nix

+4 −6
Original line number Diff line number Diff line
@@ -16,7 +16,6 @@ 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")
@@ -24,8 +23,8 @@ let 
    ] null;

  location = {

    domain = "github.com";

    owner = "coq-community";

    repo = "vscoq";

    owner = "rocq-prover";

    repo = "vsrocq";

  };

  fetch = metaFetch {

    release."2.0.3+coq8.18".sha256 = "sha256-VXhHCP6Ni5/OcsgoI1EbJfYCpXzwkuR8kbbKrl6dfjU=";
@@ -42,8 +41,7 @@ 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=";

    # This is the last version of VsCoq. Now, new versions are for VsRocq.

    inherit location;

  };

  fetched = fetch (if version != null then version else defaultVersion);
@@ -79,7 +77,7 @@ ocamlPackages.buildDunePackage { 


  meta = {

    description = "Language server for the vscoq vscode/codium extension";

    homepage = "https://github.com/coq-community/vscoq";

    homepage = "https://github.com/rocq-prover/vsrocq";

    maintainers = with lib.maintainers; [ cohencyril ];

    license = lib.licenses.mit;

  }

pkgs/development/rocq-modules/vsrocq-language-server/default.nix

+4 −3
Original line number Diff line number Diff line
@@ -16,8 +16,8 @@ let 
      case = case: out: { inherit case out; };

    in

    lib.switch rocq-core.rocq-version [

      (case (lib.versions.range "8.18" "9.1") "2.3.3")

      (case (lib.versions.range "8.18" "9.1") "2.3.0")

      # When updating the default version here, also update the VsRocq VS Code extension

      (case (lib.versions.range "8.18" "9.1") "2.3.4")

    ] null;

  location = {

    domain = "github.com";
@@ -29,6 +29,8 @@ let 
    release."2.3.0".sha256 = "sha256-BZLxcCmSGFf04eUmlJXnyxmg4hTwpFaPaIik4VD444M=";

    release."2.3.3".rev = "v2.3.3";

    release."2.3.3".sha256 = "sha256-wgn28wqWhZS4UOLUblkgXQISgLV+XdSIIEMx9uMT/ig=";

    release."2.3.4".rev = "v2.3.4";

    release."2.3.4".sha256 = "sha256-v1hQjE8U1o2VYOlUjH0seIsNG+NrMNZ8ixt4bQNyGvI=";

    inherit location;

  };

  fetched = fetch (if version != null then version else defaultVersion);
@@ -72,7 +74,6 @@ ocamlPackages.buildDunePackage { 
    license = lib.licenses.mit;

  }

  // lib.optionalAttrs (fetched.broken or false) {

    rocqFilter = true;

    broken = true;

  };

}

pkgs/top-level/coq-packages.nix

+1 −0
Original line number Diff line number Diff line
@@ -233,6 +233,7 @@ let 
      Vpl = callPackage ../development/coq-modules/Vpl { };

      VplTactic = callPackage ../development/coq-modules/VplTactic { };

      vscoq-language-server = callPackage ../development/coq-modules/vscoq-language-server { };

      vsrocq-language-server = callPackage ../development/rocq-modules/vsrocq-language-server { };

      VST = callPackage ../development/coq-modules/VST (

        (lib.optionalAttrs (lib.versionAtLeast self.coq.version "8.14") {

          compcert = self.compcert.override {