summary refs log tree commit diff
path: root/pkgs/top-level/coq-packages.nix
diff options
context:
space:
mode:
authorThéo Zimmermann <theo.zimmermann@inria.fr>2021-06-14 14:21:41 +0200
committerGitHub <noreply@github.com>2021-06-14 14:21:41 +0200
commit2bbf6c86876ecf75fe0ed1d8e3dff413bf255024 (patch)
tree409de0733b8a3bbb10f6a89e46385bd900e17de5 /pkgs/top-level/coq-packages.nix
parent19c5fd76f885e63ee030037254cc93d1006f3387 (diff)
downloadnixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar
nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.gz
nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.bz2
nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.lz
nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.xz
nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.zst
nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.zip
Move CompCert into coqPackages. (#126214)
* compcert: preparation to move in coqPackages

* compcert: move into coqPackages

* compcert: remove version 3.7

As a consequence, also remove VST version 2.6

These were broken.
Diffstat (limited to 'pkgs/top-level/coq-packages.nix')
-rw-r--r--pkgs/top-level/coq-packages.nix14
1 files changed, 7 insertions, 7 deletions
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 1ac8c4c4005..fb7e2113018 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -1,5 +1,5 @@
-{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
-, ocamlPackages_4_10, compcert
+{ lib, stdenv, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
+, ocamlPackages_4_10, fetchpatch, makeWrapper, coq2html
 }@args:
 let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
 let
@@ -21,6 +21,10 @@ let
       category-theory = callPackage ../development/coq-modules/category-theory { };
       Cheerios = callPackage ../development/coq-modules/Cheerios {};
       CoLoR = callPackage ../development/coq-modules/CoLoR {};
+      compcert = callPackage ../development/coq-modules/compcert {
+        ocamlPackages = ocamlPackages_4_05;
+        inherit fetchpatch makeWrapper coq2html lib stdenv;
+      };
       coq-bits = callPackage ../development/coq-modules/coq-bits {};
       coq-elpi = callPackage ../development/coq-modules/coq-elpi {};
       coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
@@ -78,11 +82,7 @@ let
       topology = callPackage ../development/coq-modules/topology {};
       Velisarios = callPackage ../development/coq-modules/Velisarios {};
       Verdi = callPackage ../development/coq-modules/Verdi {};
-      VST = callPackage ../development/coq-modules/VST (with lib.versions;
-        lib.switch coq.coq-version [
-          { case = "8.11"; out = { compcert = compcert.override { coqPackages = self; version = "3.7"; }; }; }
-          { case = range "8.12" "8.13"; out = { compcert = compcert.override { coqPackages = self; version = "3.8"; }; }; }
-        ] {});
+      VST = callPackage ../development/coq-modules/VST {};
       zorns-lemma = callPackage ../development/coq-modules/zorns-lemma {};
       filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
     };