Merge 8.16, 8.17 and 8.18 into main #993

yforster · 2023-10-16T13:39:24Z

No description provided.

This is useful for managing global envs around Gallina quotation.

This will allow programatically combining checker flags from multiple constants in Gallina quotation.

This will be useful for proving that quotation of byte is well-typed with the safechecker.

Add MCListable class for enumerating finite types

Close computational obligations with defined in erase_global_decls

Bumps [cachix/install-nix-action](https://github.com/cachix/install-nix-action) from 20 to 21. - [Release notes](https://github.com/cachix/install-nix-action/releases) - [Commits](cachix/install-nix-action@v20...v21) --- updated-dependencies: - dependency-name: cachix/install-nix-action dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

Add a merge operation for the global env

Bumps [cachix/install-nix-action](https://github.com/cachix/install-nix-action) from 21 to 22. - [Release notes](https://github.com/cachix/install-nix-action/releases) - [Commits](cachix/install-nix-action@v21...v22) --- updated-dependencies: - dependency-name: cachix/install-nix-action dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] <[email protected]> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

improve strengthening to get cumul info on type

…positionally

…ning to a first step

… relation

Verified erasure pipeline

add not_isErasable lemma in EArities

SkySkimmer · 2023-10-17T12:01:31Z

erasure/theories/ErasureFunction.v

+
+    + intros hl.
+      case: (knset_mem_spec kn0 _) => hin.
+      * elimtype False.


elimtype doesn't exist anymore

SkySkimmer · 2023-10-17T12:02:05Z

This broke Coq master

JasonGross · 2023-10-17T13:51:40Z

coq-metacoq-common.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev"
+version: "8.18.dev"


This seems backwards

JasonGross · 2023-10-17T13:51:50Z

coq-metacoq-erasure-plugin.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev"
+version: "8.18.dev"


JasonGross · 2023-10-17T13:52:00Z

coq-metacoq-erasure.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev"
+version: "8.18.dev"


JasonGross · 2023-10-17T13:52:12Z

coq-metacoq-pcuic.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev"
+version: "8.18.dev"


JasonGross · 2023-10-17T13:52:24Z

coq-metacoq-quotation.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev"
+version: "8.18.dev"


JasonGross · 2023-10-17T13:53:23Z

coq-metacoq-utils.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev"
+version: "8.18.dev"


JasonGross · 2023-10-17T13:54:02Z

coq-metacoq-utils.opam

-  "coq" { = "dev" }
-  "coq-equations" { = "dev" }
+  "coq" { >= "8.18" & < "8.19~" }
+  "coq-equations" { = "1.3+8.18" }


This change is breaking CI, as is the line above it

JasonGross · 2023-10-17T13:54:13Z

coq-metacoq.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "dev"
+version: "8.18.dev"


JasonGross · 2023-10-17T13:55:10Z

.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


Is this a merge artifact?

JasonGross · 2023-10-17T13:55:28Z

.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


And this too

JasonGross and others added 30 commits April 23, 2023 12:33

Fix monad_map_branches_k name (#953)

46454e2

Add boolean versions of the varieties of extends (#954)

d8f1479

Add a merge operation for the global env

dd8c80d

This is useful for managing global envs around Gallina quotation.

Add computable version of Env compatibility; refactor extension a bit

7ea63fa

More extension lemmas

6ddfd13

Fix issue with hint breaking a proof

6307467

Add union and inter checker flags (#957)

6c63eac

This will allow programatically combining checker flags from multiple constants in Gallina quotation.

Fix sprop_level/prop_level requring lazy evaluation

198e202

Fix use of lazy for (s)prop_level

c7b8d8f

close some computational obligations with defined in erase_global_decls

f91a1e7

Add MCListable class for enumerating finite types

e04bc87

This will be useful for proving that quotation of byte is well-typed with the safechecker.

Merge pull request #962 from JasonGross/coq-8.16+listable

c67d968

Add MCListable class for enumerating finite types

Move nix actions away

e578a02

Merge pull request #961 from yforster/fix-qed-problem

bb34a12

Close computational obligations with defined in erase_global_decls

Invariants in named recursion rule (#967)

14ad024

Merge pull request #955 from JasonGross/coq-8.16+global-env-merge

f1f2028

Add a merge operation for the global env

Fix a sneaky Prop <= Type use messing up certified erasure

6899a1a

Update Makefile to install erasure plugin

c065ed6

Fix sneaky, useless Prop <= Type use that was breaking certified erasure

e0794e3

Update dependabot.yml to also update other branches

f5967d8

Update dependabot.yml to check main, not master

a738c55

Bump actions/checkout from 3 to 4 (#978)

3e0f857

Bump actions/checkout from 3 to 4 (#977)

555b239

Bump cachix/install-nix-action from 22 to 23 (#979)

7723421

improve stengthening to get cumul info on type

adba794

more general strengthening

9fd6f61

Merge pull request #985 from MetaCoq/improve-strengthening

46be926

improve strengthening to get cumul info on type

mattam82 and others added 23 commits October 2, 2023 16:23

Finished proof of firstorder correctness for erase_pcuic_program

80055db

Modify Transform class to allow showing preservation of fo values com…

0934fc0

…positionally

Proved most of the fo preservation of the lambdabox pipeline

1f1248d

Finish main erasure correctness proof. Need to move expand_lets reaso…

0e5938a

…ning to a first step

We're missing preservation of eta-expandedness by reduction in PCUIC...

915ce93

Prove preservation of expansion by reduction using a custom reduction…

f169916

… relation

Finished preservation of expansion proof

2f5fed3

Refactor a bit, work on side conditions for let expansion

681a382

Filled all proofs in ErasureCorrectness

b072acf

Cleanup a bit, remain only normalization side-conditions

708302f

Fix erasure plugin compilation

a0dc628

Cleanup

487cdf5

Minor fixes

dfb03d1

fix CI

efe2b96

Fix after rebase

f2b1cc0

Fix test suite

357e8a7

Merge pull request #987 from MetaCoq/verified_erasure_pipeline

3733e67

Verified erasure pipeline

coq-equations.1.3+8.18

1fcd7ff

add not_isErasable lemma in EArities

1dc7961

Merge pull request #990 from MetaCoq/not_isErasable

65e8a93

add not_isErasable lemma in EArities

Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17

241dd7f

fix Makefile

34c831e

Merge branch 'coq-8.17-updates-8.16' into coq-8.18

87f8ebf

yforster changed the title ~~Main updates 8.18~~ Merge 8.16, 8.17 and 8.18 into main Oct 16, 2023

Remove nix

97911f2

yforster merged commit adc980c into main Oct 16, 2023
11 of 12 checks passed

yforster deleted the main-updates-8.18 branch October 16, 2023 15:11

SkySkimmer reviewed Oct 17, 2023

View reviewed changes

JasonGross reviewed Oct 17, 2023

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Merge 8.16, 8.17 and 8.18 into main #993

Merge 8.16, 8.17 and 8.18 into main #993

yforster commented Oct 16, 2023

SkySkimmer Oct 17, 2023

SkySkimmer commented Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

JasonGross Oct 17, 2023

Merge 8.16, 8.17 and 8.18 into main #993

Merge 8.16, 8.17 and 8.18 into main #993

Conversation

yforster commented Oct 16, 2023

Choose a reason for hiding this comment

SkySkimmer commented Oct 17, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment