one package by plugin

Author: tabareau

.github/workflows/nix-action-coq-8.16-macos.yml

@@ -147,9 +147,13 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "metacoq-template-pcuic"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: metacoq-plugins'
+      name: 'Building/fetching previous CI target: metacoq-safechecker-plugin'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
-        --argstr job "metacoq-plugins"
+        --argstr job "metacoq-safechecker-plugin"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-erasure-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-erasure-plugin"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"

.github/workflows/nix-action-coq-8.16-ubuntu.yml

@@ -147,9 +147,13 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
         --argstr job "metacoq-template-pcuic"
     - if: steps.stepCheck.outputs.status == 'built'
-      name: 'Building/fetching previous CI target: metacoq-plugins'
+      name: 'Building/fetching previous CI target: metacoq-safechecker-plugin'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
-        --argstr job "metacoq-plugins"
+        --argstr job "metacoq-safechecker-plugin"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-erasure-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"
+        --argstr job "metacoq-erasure-plugin"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16"

.nix/coq-overlays/metacoq/default.nix

@@ -25,7 +25,7 @@ let
   releaseRev = v: "v${v}";
 
   # list of core metacoq packages sorted by dependency order
-  packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "erasure" "template-pcuic" "plugins" "all" ];
+  packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "erasure" "template-pcuic" "safechecker-plugin" "erasure-plugin" "all" ];
 
   template-coq = metacoq_ "template-coq";
 
@@ -57,7 +57,7 @@ let
 
         configurePhase = optionalString (package == "all") pkgallMake + ''
           touch ${pkgpath}/metacoq-config
-        '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "plugins"]) ''
+        '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "safechecker-plugin" "erasure-plugin"]) ''
           echo  "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
         '' + optionalString (package == "single") ''
           ./configure.sh local

coq-metacoq-plugins.opam renamed to coq-metacoq-erasure-plugin.opam

@@ -21,11 +21,9 @@ authors: ["Abhishek Anand <[email protected]>"
 license: "MIT"
 build: [
   ["bash" "./configure.sh"]
-  [make "-j" "%{jobs}%" "-C" "safechecker-plugin"]
   [make "-j" "%{jobs}%" "-C" "erasure-plugin"]
 ]
 install: [
-  [make "-C" "safechecker-plugin" "install"]
   [make "-C" "erasure-plugin" "install"]
 ]
 depends: [

coq-metacoq-safechecker-plugin.opam

@@ -0,0 +1,43 @@
+opam-version: "2.0"
+version: "8.16.dev"
+maintainer: "[email protected]"
+homepage: "https://metacoq.github.io/metacoq"
+dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16"
+bug-reports: "https://github.com/MetaCoq/metacoq/issues"
+authors: ["Abhishek Anand <[email protected]>"
+          "Danil Annenkov <[email protected]>"
+          "Simon Boulier <[email protected]>"
+          "Cyril Cohen <[email protected]>"
+          "Yannick Forster <[email protected]>"
+          "Fabian Kunze <[email protected]>"
+          "Meven Lennon-Bertrand <[email protected]>"
+          "Kenji Maillard <[email protected]>"
+          "Gregory Malecha <[email protected]>"
+          "Jakob Botsch Nielsen <[email protected]>"
+          "Matthieu Sozeau <[email protected]>"
+          "Nicolas Tabareau <[email protected]>"
+          "Théo Winterhalter <[email protected]>"
+]
+license: "MIT"
+build: [
+  ["bash" "./configure.sh"]
+  [make "-j" "%{jobs}%" "-C" "safechecker-plugin"]
+]
+install: [
+  [make "-C" "safechecker-plugin" "install"]
+]
+depends: [
+  "coq-metacoq-template-pcuic" {= version}
+]
+synopsis: "Implementation and verification of an erasure procedure for Coq"
+description: """
+MetaCoq is a meta-programming framework for Coq.
+
+The Erasure module provides a complete specification of Coq's so-called
+\"extraction\" procedure, starting from the PCUIC calculus and targeting
+untyped call-by-value lambda-calculus.
+
+The `erasure` function translates types and proofs in well-typed terms
+into a dummy `tBox` constructor, following closely P. Letouzey's PhD
+thesis.
+"""

coq-metacoq.opam

@@ -20,7 +20,8 @@ authors: ["Abhishek Anand <[email protected]>"
 ]
 license: "MIT"
 depends: [
-  "coq-metacoq-plugins" {= version}
+  "coq-metacoq-safechecker-plugin" {= version}
+  "coq-metacoq-erasure-plugin" {= version}
   "coq-metacoq-translations" {= version}
 ]
 build: [