Merge pull request #745 from kyoDralliam/positivity-cleanups

Fix issues with nix workflow
MetaCoq · Sep 13, 2022 · 9bf9f6a · 9bf9f6a
2 parents 6db5f24 + 23a15e7
commit 9bf9f6a
Show file tree

Hide file tree

Showing 5 changed files with 64 additions and 5 deletions.
diff --git a/.github/workflows/nix-action-default-macos.yml b/.github/workflows/nix-action-default-macos.yml
@@ -36,7 +36,8 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
         --argstr job "coq"
   equations:
-    needs: []
+    needs:
+    - coq
     runs-on: macos-latest
     steps:
     - name: Determine which commit to test
@@ -67,12 +68,17 @@ jobs:
         \ bundle \"default\" --argstr job \"equations\" \\\n   --dry-run 2>&1 > /dev/null)\n\
         echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
         \ \"built:\" | sed \"s/.*/built/\")\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "coq"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
         --argstr job "equations"
   metacoq:
     needs:
+    - coq
     - equations
     runs-on: macos-latest
     steps:
@@ -104,10 +110,30 @@ jobs:
         \ bundle \"default\" --argstr job \"metacoq\" \\\n   --dry-run 2>&1 > /dev/null)\n\
         echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
         \ \"built:\" | sed \"s/.*/built/\")\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "coq"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: equations'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
         --argstr job "equations"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-template-coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "metacoq-template-coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-pcuic'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "metacoq-pcuic"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-safechecker'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "metacoq-safechecker"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-erasure'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "metacoq-erasure"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"

diff --git a/.github/workflows/nix-action-default-ubuntu.yml b/.github/workflows/nix-action-default-ubuntu.yml
@@ -36,7 +36,8 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
         --argstr job "coq"
   equations:
-    needs: []
+    needs:
+    - coq
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to test
@@ -67,12 +68,17 @@ jobs:
         \ bundle \"default\" --argstr job \"equations\" \\\n   --dry-run 2>&1 > /dev/null)\n\
         echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
         \ \"built:\" | sed \"s/.*/built/\")\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "coq"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
         --argstr job "equations"
   metacoq:
     needs:
+    - coq
     - equations
     runs-on: ubuntu-latest
     steps:
@@ -104,10 +110,30 @@ jobs:
         \ bundle \"default\" --argstr job \"metacoq\" \\\n   --dry-run 2>&1 > /dev/null)\n\
         echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
         \ \"built:\" | sed \"s/.*/built/\")\n"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "coq"
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: equations'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
         --argstr job "equations"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-template-coq'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "metacoq-template-coq"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-pcuic'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "metacoq-pcuic"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-safechecker'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "metacoq-safechecker"
+    - if: steps.stepCheck.outputs.status == 'built'
+      name: 'Building/fetching previous CI target: metacoq-erasure'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"
+        --argstr job "metacoq-erasure"
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default"

diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"3fab39da659da297a9633cf0d53c8dcb5a8f24ad"
+"39243d0edb4cb0b872d299c4b128fe232f0d8101"
diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix
@@ -1,4 +1,4 @@
 fetchTarball {
-    url = https://github.com/NixOS/nixpkgs/archive/34e4df55664c24df350f59adba8c7a042dece61e.tar.gz;
-    sha256 = "0z313l585blzzj17gnaqi41j3z24gb9ivjdjvqx3r8xwlh0n4b3i";
+    url = https://github.com/NixOS/nixpkgs/archive/fbac99137c1276ac8aa41d91b4997feaeab256a3.tar.gz;
+    sha256 = "1dkj2b03zxy8c7cp2bs1yjlrg4zwnhb292w6v8h1zav0c3apv2m8";
   }
diff --git a/safechecker/theories/PCUICErrors.v b/safechecker/theories/PCUICErrors.v
@@ -363,6 +363,13 @@ Inductive env_error :=
 | IllFormedDecl (e : string) (e : type_error)
 | AlreadyDeclared (id : string).
 
+Definition string_of_env_error Σ (e : env_error) :=
+  match e with
+  | IllFormedDecl decl_name typ_error =>
+      "Type error on " ^ decl_name ^ " " ^ string_of_type_error Σ typ_error
+  | AlreadyDeclared decl_name =>
+      "Name is already declared in environment " ^ decl_name
+  end.
 
 Section EnvCheck.