Merge pull request #991 from MetaCoq/coq-8.18-updates-8.17

.github/dependabot.yml

@@ -9,3 +9,27 @@ updates:
       interval: "daily"
     labels:
       - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "main"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "coq-8.17"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    target-branch: "coq-8.16"
+    schedule:
+      # Check for updates to GitHub Actions every weekday
+      interval: "daily"
+    labels:
+      - "dependencies"

.github/workflows/nix-action-coq-dev-macos.yml → .github/nix-action-coq-8.17-macos.yml

@@ -19,7 +19,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-macos.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-macos.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq
@@ -59,7 +63,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-macos.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-macos.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq
@@ -104,7 +112,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-macos.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-macos.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq

.github/workflows/nix-action-coq-dev-ubuntu.yml → .github/nix-action-coq-8.17-ubuntu.yml

@@ -19,7 +19,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-ubuntu.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-ubuntu.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq
@@ -59,7 +63,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-ubuntu.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-ubuntu.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq
@@ -104,7 +112,11 @@ jobs:
         fetch-depth: 0
         ref: ${{ env.tested_commit }}
     - name: Cachix install
+<<<<<<<< HEAD:.github/workflows/nix-action-coq-dev-ubuntu.yml
       uses: cachix/install-nix-action@v22
+========
+      uses: cachix/install-nix-action@v23
+>>>>>>>> coq-8.17-updates-8.16:.github/nix-action-coq-8.17-ubuntu.yml
       with:
         nix_path: nixpkgs=channel:nixpkgs-unstable
     - name: Cachix setup metacoq

.gitignore

@@ -405,3 +405,5 @@ erasure-plugin/Makefile.erasureplugin
 erasure-plugin/Makefile.erasureplugin.conf
 erasure-plugin/Makefile.plugin
 erasure-plugin/Makefile.plugin.conf
+erasure-plugin/META
+safechecker-plugin/META

.vscode/metacoq.code-workspace

@@ -10,6 +10,7 @@
         "coqtop.args": [
 
 
+
 			"-R", "safechecker-plugin/theories", "MetaCoq.SafeCheckerPlugin",
 
 			"-R", "utils/theories", "MetaCoq.Utils",
@@ -27,6 +28,7 @@
 		"-R", "safechecker/theories", "MetaCoq.SafeChecker",
 		"-I", "erasure/src",
 		"-R", "erasure/theories", "MetaCoq.Erasure",
+		"-R", "erasure-plugin/theories", "MetaCoq.ErasurePlugin",
 		"-R", "translations", "MetaCoq.Translations",
 		"-R", "test-suite/plugin-demo/theories", "MetaCoq.ExtractedPluginDemo",
 		"-R", "test-suite", "MetaCoq.TestSuite"

Makefile

@@ -1,5 +1,5 @@
 
-all: printconf template-coq pcuic safechecker erasure examples test-suite translations quotation
+all: printconf template-coq pcuic safechecker erasure erasure-plugin 
 
 -include Makefile.conf
 
@@ -26,7 +26,7 @@ else
 endif
 endif
 
-install: all translations
+install: all 
 	$(MAKE) -C utils install
 	$(MAKE) -C common install
 	$(MAKE) -C template-coq install
@@ -36,7 +36,7 @@ install: all translations
 	$(MAKE) -C quotation install
 	$(MAKE) -C safechecker-plugin install
 	$(MAKE) -C erasure install
-	$(MAKE) -C translations install
+	$(MAKE) -C erasure-plugin install
 
 uninstall:
 	$(MAKE) -C utils uninstall
@@ -48,6 +48,7 @@ uninstall:
 	$(MAKE) -C quotation uninstall
 	$(MAKE) -C safechecker-plugin uninstall
 	$(MAKE) -C erasure uninstall
+	$(MAKE) -C erasure-plugin uninstall
 	$(MAKE) -C translations uninstall
 
 html: all
@@ -175,7 +176,7 @@ cleanplugins:
 
 ci-local-noclean:
 	./configure.sh local
-	$(MAKE) all test-suite TIMED=pretty-timed
+	$(MAKE) all translations test-suite TIMED=pretty-timed
 
 ci-local: ci-local-noclean
 	$(MAKE) clean

common/_CoqProject.in

@@ -11,5 +11,6 @@ theories/MonadBasicAst.v
 theories/Environment.v
 theories/Reflect.v
 theories/EnvironmentTyping.v
+theories/EnvironmentReflect.v
 theories/EnvMap.v
 theories/Transform.v