Code

Merge 8.16, 8.17 and 8.18 into main#993

Code

Merged

yforster merged 75 commits intomainMetaCoq/metacoq:mainfrom main-updates-8.18MetaCoq/metacoq:main-updates-8.18Copy head branch name to clipboardOct 16, 2023

+9,673-3,127

Commits

Commits on Apr 23, 2023

• Fix monad_map_branches_k name (#953)

  JasonGross

  authored
  46454e2

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

  JasonGross

  authored
  d8f1479

• Add a merge operation for the global env

  Show description for dd8c80d
  JasonGross

  committed
  dd8c80d

• Add computable version of Env compatibility; refactor extension a bit

  JasonGross

  committed
  7ea63fa

Commits on Apr 24, 2023

• More extension lemmas

  JasonGross

  committed
  6ddfd13

• Fix issue with hint breaking a proof

  JasonGross

  committed
  6307467

Commits on May 3, 2023

• Add union and inter checker flags (#957)

  Show description for 6c63eac
  JasonGross

  authored
  6c63eac

Commits on May 5, 2023

• Fix sprop_level/prop_level requring lazy evaluation

  mattam82

  committed
  198e202

• Fix use of lazy for (s)prop_level

  mattam82

  committed
  c7b8d8f

• close some computational obligations with defined in erase_global_decls

  yforster

  committed
  f91a1e7

Commits on May 6, 2023

• Add MCListable class for enumerating finite types

  Show description for e04bc87
  JasonGross

  committed
  e04bc87

Commits on May 9, 2023

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

  Show description for c67d968
  tabareau

  authored
  c67d968

• Move nix actions away

  mattam82

  committed
  e578a02

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

  Show description for bb34a12
  mattam82

  authored
  bb34a12

Commits on Jun 2, 2023

• Invariants in named recursion rule (#967)

  yforster

  authored
  14ad024

Commits on Jun 19, 2023

• Bump cachix/install-nix-action from 20 to 21 (#966)

  Show description for 713dbde
  dependabot[bot]

  authored
  713dbde

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

  Show description for f1f2028
  yforster

  authored
  f1f2028

Commits on Jun 28, 2023

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

  mattam82

  committed
  6899a1a

• Update Makefile to install erasure plugin

  mattam82

  committed
  c065ed6

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

  mattam82

  committed
  e0794e3

Commits on Jul 5, 2023

• Update dependabot.yml to also update other branches

  JasonGross

  authored
  f5967d8

• Update dependabot.yml to check main, not master

  JasonGross

  authored
  a738c55

• Bump cachix/install-nix-action from 21 to 22 (#970)

  Show description for e8d0b36
  dependabot[bot]

  authored
  e8d0b36

• Bump cachix/install-nix-action from 21 to 22 (#973)

  Show description for 943cc72
  dependabot[bot]

  authored
  943cc72

Commits on Sep 4, 2023

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

  dependabot[bot]

  authored
  3e0f857

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

  dependabot[bot]

  authored
  555b239

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

  dependabot[bot]

  authored
  7723421

Commits on Sep 26, 2023

• improve stengthening to get cumul info on type

  tabareau

  committed
  adba794

• more general strengthening

  tabareau

  committed
  9fd6f61

Commits on Sep 27, 2023

• Merge pull request #985 from MetaCoq/improve-strengthening

  Show description for 46be926
  tabareau

  authored
  46be926

• remove parameters in firstorder inductive types

  tabareau

  committed
  be44477

Commits on Sep 28, 2023

• Merge pull request #986 from MetaCoq/remove-parameters-in-firstorder-inductive-types

  Show description for a152eec
  tabareau

  authored
  a152eec

Commits on Sep 30, 2023

• Drastically speed up ByteCompareSpec

  Show description for 00a4299
  JasonGross

  committed
  00a4299

Commits on Oct 2, 2023

• Merge pull request #988 from JasonGross/coq-8.16+bytecomparespec-better

  Show description for 9f7cc51
  ppedrot

  authored
  9f7cc51

• adapt CI and opam files to 8.18

  yforster

  committed
  c2d2754

• update documentation to mention 8.18

  yforster

  committed
  88b4a4d

• split out verified erasure pipeline

  

  yforster

  authored and

  mattam82

  committed
  dce0b9e

• Add pass implementing boxes as fixpoints

  

  yforster

  authored and

  mattam82

  committed
  a813bff

• adapt name pass to not consider box

  

  yforster

  authored and

  mattam82

  committed
  5bc51f5

• remove assumption

  

  yforster

  authored and

  mattam82

  committed
  7565dd4

• Fix definition of Transform.t's observational equivalence preservation

  mattam82

  committed
  a359961

• prove wellformedness of annotate

  

  yforster

  authored and

  mattam82

  committed
  06ca492

• wellformed_annotate_env

  

  yforster

  authored and

  mattam82

  committed
  f1a2548

• WIP stronger global weakening theorems for optimizations

  mattam82

  committed
  6a1428a

• Allow modifying inductive decls in generic weakenability translation proofs.

  Show description for e09e64d
  mattam82

  committed
  e09e64d

• Prove a more precise result about erase_global_decls with dependencies

  mattam82

  committed
  805bbda

• No need for ext proof for erasure

  mattam82

  committed
  8710ece

• Strenghtened program extension preservation

  mattam82

  committed
  7158506

• Progress on pipeline theorem proof, main argument remains

  mattam82

  committed
  3856b00

• Main argument of the erasure with dependencies proof

  mattam82

  committed
  71819e7

• Finish the proofs in ErasureFunction

  mattam82

  committed
  93395bf

• Finished proof of firstorder correctness for erase_pcuic_program

  mattam82

  committed
  80055db

• Modify Transform class to allow showing preservation of fo values compositionally

  mattam82

  committed
  0934fc0

• Proved most of the fo preservation of the lambdabox pipeline

  mattam82

  committed
  1f1248d

• Finish main erasure correctness proof. Need to move expand_lets reasoning to a first step

  mattam82

  committed
  0e5938a

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

  mattam82

  committed
  915ce93

• Prove preservation of expansion by reduction using a custom reduction relation

  mattam82

  committed
  f169916

• Finished preservation of expansion proof

  mattam82

  committed
  2f5fed3

• Refactor a bit, work on side conditions for let expansion

  mattam82

  committed
  681a382

• Filled all proofs in ErasureCorrectness

  mattam82

  committed
  b072acf

• Cleanup a bit, remain only normalization side-conditions

  mattam82

  committed
  708302f

• Fix erasure plugin compilation

  mattam82

  committed
  a0dc628

• Cleanup

  mattam82

  committed
  487cdf5

• Minor fixes

  mattam82

  committed
  dfb03d1

• fix CI

  yforster

  committed
  efe2b96

Commits on Oct 3, 2023

• Fix after rebase

  mattam82

  committed
  f2b1cc0

• Fix test suite

  mattam82

  committed
  357e8a7

• Merge pull request #987 from MetaCoq/verified_erasure_pipeline

  Show description for 3733e67
  mattam82

  authored
  3733e67

Commits on Oct 5, 2023

• coq-equations.1.3+8.18

  yforster

  committed
  1fcd7ff

Commits on Oct 10, 2023

• add not_isErasable lemma in EArities

  tabareau

  committed
  1dc7961

• Merge pull request #990 from MetaCoq/not_isErasable

  Show description for 65e8a93
  tabareau

  authored
  65e8a93

Commits on Oct 16, 2023

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

  yforster

  committed
  241dd7f

• fix Makefile

  yforster

  committed
  34c831e

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

  yforster

  committed
  87f8ebf

• Remove nix

  yforster

  committed
  97911f2