Code

Stack overflow 8.17#1017

Code

Closed

mattam82 wants to merge 104 commits intocoq-8.16MetaCoq/metacoq:coq-8.16from stack-overflow-8.17MetaCoq/metacoq:stack-overflow-8.17Copy head branch name to clipboard

+15,621-4,144

Commits

Commits on Apr 4, 2023

• improved auto goal selection (#737)

  

  mrhaandi

  authored and

  mattam82

  committed
  1a7d230

  Copy full SHA for 1a7d230

Commits on Apr 5, 2023

• prepare for coq/coq#16289 (#734)

  

  mrhaandi

  authored and

  mattam82

  committed
  7d1b643

  Copy full SHA for 7d1b643

Commits on Apr 13, 2023

• Adapt w.r.t. coq/coq#16442.

  

  ppedrot

  authored and

  mattam82

  committed
  2e1085a

  Copy full SHA for 2e1085a

• ML fixes

  mattam82

  committed
  6219522

  Copy full SHA for 6219522

• Adapt to Coq 8.17

  mattam82

  committed
  7399921

  Copy full SHA for 7399921

• Update opam packages

  mattam82

  committed
  0d08380

  Copy full SHA for 0d08380

• Update github action coq version

  mattam82

  committed
  6f72fe9

  Copy full SHA for 6f72fe9

Commits on Apr 14, 2023

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

  mattam82

  committed
  83cea47

  Copy full SHA for 83cea47

• Usage for make-opam-files

  mattam82

  committed
  66e7d31

  Copy full SHA for 66e7d31

• Fix dep in opam file

  mattam82

  committed
  76e8e48

  Copy full SHA for 76e8e48

Commits on Apr 17, 2023

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

  mattam82

  committed
  ea7b244

  Copy full SHA for ea7b244

Commits on Apr 18, 2023

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

  mattam82

  committed
  4b975ae

  Copy full SHA for 4b975ae

• Fix due to high priority existT hint in core

  mattam82

  committed
  66f6857

  Copy full SHA for 66f6857

Commits on Apr 19, 2023

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

  mattam82

  committed
  f867f01

  Copy full SHA for f867f01

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

  mattam82

  committed
  e61cd19

  Copy full SHA for e61cd19

Commits on Apr 20, 2023

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

  mattam82

  committed
  736ac17

  Copy full SHA for 736ac17

• Update install instructions for Coq 8.17

  mattam82

  committed
  1f9ed65

  Copy full SHA for 1f9ed65

Commits on Apr 22, 2023

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

  mattam82

  committed
  c27c302

  Copy full SHA for c27c302

Commits on May 5, 2023

• Fix sprop_level/prop_level requring lazy evaluation

  mattam82

  committed
  198e202

  Copy full SHA for 198e202

• close some computational obligations with defined in erase_global_decls

  yforster

  committed
  f91a1e7

  Copy full SHA for f91a1e7

Commits on May 9, 2023

• Move nix actions away

  mattam82

  committed
  e578a02

  Copy full SHA for e578a02

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

  Show description for bb34a12
  mattam82

  authored
  bb34a12

  Copy full SHA for bb34a12

Commits on Jun 2, 2023

• Invariants in named recursion rule (#967)

  yforster

  authored
  14ad024

  Copy full SHA for 14ad024

Commits on Jun 28, 2023

• Update Makefile to install erasure plugin

  mattam82

  committed
  c065ed6

  Copy full SHA for c065ed6

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

  mattam82

  committed
  e0794e3

  Copy full SHA for e0794e3

Commits on Sep 4, 2023

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

  dependabot[bot]

  authored
  3e0f857

  Copy full SHA for 3e0f857

Commits on Sep 26, 2023

• improve stengthening to get cumul info on type

  tabareau

  committed
  adba794

  Copy full SHA for adba794

• more general strengthening

  tabareau

  committed
  9fd6f61

  Copy full SHA for 9fd6f61

Commits on Sep 27, 2023

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

  Show description for 46be926
  tabareau

  authored
  46be926

  Copy full SHA for 46be926

• remove parameters in firstorder inductive types

  tabareau

  committed
  be44477

  Copy full SHA for 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

  Copy full SHA for a152eec

Commits on Oct 2, 2023

• split out verified erasure pipeline

  

  yforster

  authored and

  mattam82

  committed
  dce0b9e

  Copy full SHA for dce0b9e

• Add pass implementing boxes as fixpoints

  

  yforster

  authored and

  mattam82

  committed
  a813bff

  Copy full SHA for a813bff

• adapt name pass to not consider box

  

  yforster

  authored and

  mattam82

  committed
  5bc51f5

  Copy full SHA for 5bc51f5

• remove assumption

  

  yforster

  authored and

  mattam82

  committed
  7565dd4

  Copy full SHA for 7565dd4

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

  mattam82

  committed
  a359961

  Copy full SHA for a359961

• prove wellformedness of annotate

  

  yforster

  authored and

  mattam82

  committed
  06ca492

  Copy full SHA for 06ca492

• wellformed_annotate_env

  

  yforster

  authored and

  mattam82

  committed
  f1a2548

  Copy full SHA for f1a2548

• WIP stronger global weakening theorems for optimizations

  mattam82

  committed
  6a1428a

  Copy full SHA for 6a1428a

• Allow modifying inductive decls in generic weakenability translation proofs.

  Show description for e09e64d
  mattam82

  committed
  e09e64d

  Copy full SHA for e09e64d

• Prove a more precise result about erase_global_decls with dependencies

  mattam82

  committed
  805bbda

  Copy full SHA for 805bbda

• No need for ext proof for erasure

  mattam82

  committed
  8710ece

  Copy full SHA for 8710ece

• Strenghtened program extension preservation

  mattam82

  committed
  7158506

  Copy full SHA for 7158506

• Progress on pipeline theorem proof, main argument remains

  mattam82

  committed
  3856b00

  Copy full SHA for 3856b00

• Main argument of the erasure with dependencies proof

  mattam82

  committed
  71819e7

  Copy full SHA for 71819e7

• Finish the proofs in ErasureFunction

  mattam82

  committed
  93395bf

  Copy full SHA for 93395bf

• Finished proof of firstorder correctness for erase_pcuic_program

  mattam82

  committed
  80055db

  Copy full SHA for 80055db

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

  mattam82

  committed
  0934fc0

  Copy full SHA for 0934fc0

• Proved most of the fo preservation of the lambdabox pipeline

  mattam82

  committed
  1f1248d

  Copy full SHA for 1f1248d

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

  mattam82

  committed
  0e5938a

  Copy full SHA for 0e5938a

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

  mattam82

  committed
  915ce93

  Copy full SHA for 915ce93

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

  mattam82

  committed
  f169916

  Copy full SHA for f169916

• Finished preservation of expansion proof

  mattam82

  committed
  2f5fed3

  Copy full SHA for 2f5fed3

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

  mattam82

  committed
  681a382

  Copy full SHA for 681a382

• Filled all proofs in ErasureCorrectness

  mattam82

  committed
  b072acf

  Copy full SHA for b072acf

• Cleanup a bit, remain only normalization side-conditions

  mattam82

  committed
  708302f

  Copy full SHA for 708302f

• Fix erasure plugin compilation

  mattam82

  committed
  a0dc628

  Copy full SHA for a0dc628

• Cleanup

  mattam82

  committed
  487cdf5

  Copy full SHA for 487cdf5

• Minor fixes

  mattam82

  committed
  dfb03d1

  Copy full SHA for dfb03d1

Commits on Oct 3, 2023

• Fix after rebase

  mattam82

  committed
  f2b1cc0

  Copy full SHA for f2b1cc0

• Fix test suite

  mattam82

  committed
  357e8a7

  Copy full SHA for 357e8a7

• Merge pull request #987 from MetaCoq/verified_erasure_pipeline

  Show description for 3733e67
  mattam82

  authored
  3733e67

  Copy full SHA for 3733e67

Commits on Oct 10, 2023

• add not_isErasable lemma in EArities

  tabareau

  committed
  1dc7961

  Copy full SHA for 1dc7961

• Merge pull request #990 from MetaCoq/not_isErasable

  Show description for 65e8a93
  tabareau

  authored
  65e8a93

  Copy full SHA for 65e8a93

Commits on Oct 16, 2023

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

  yforster

  committed
  241dd7f

  Copy full SHA for 241dd7f

• fix Makefile

  yforster

  committed
  34c831e

  Copy full SHA for 34c831e

• Merge pull request #992 from MetaCoq/coq-8.17-updates-8.16

  yforster

  authored
  1e3d82d

  Copy full SHA for 1e3d82d

Commits on Oct 26, 2023

• use names in EAst.t

  tabareau

  committed
  18a24e5

  Copy full SHA for 18a24e5

• Merge pull request #997 from MetaCoq/use-names-in-EAst

  Show description for 79f7454
  tabareau

  authored
  79f7454

  Copy full SHA for 79f7454

Commits on Nov 1, 2023

• linearize case

  yforster

  committed
  f7d27f7

  Copy full SHA for f7d27f7

• add install-plugins target in Makefile

  yforster

  committed
  7d58a86

  Copy full SHA for 7d58a86

• move implement_box_transformation to coq-malfunction

  yforster

  committed
  f8aba7c

  Copy full SHA for f8aba7c

• eliminate race condition for opam compilation

  yforster

  committed
  6d98589

  Copy full SHA for 6d98589

• disable quick target in CI - it is not quicker

  yforster

  committed
  e649edb

  Copy full SHA for e649edb

• fix Makefile and opam files

  yforster

  committed
  b33a9bd

  Copy full SHA for b33a9bd

Commits on Nov 15, 2023

• Show that applications of eta-expanded functions are preserved

  mattam82

  committed
  a6b7428

  Copy full SHA for a6b7428

• Prove app preservation for erase and let expansion

  mattam82

  committed
  9ed43d7

  Copy full SHA for 9ed43d7

• WIP on normal predicate

  mattam82

  committed
  0def703

  Copy full SHA for 0def703

• Definition of normal forms and proof that they reduce only to themselves

  mattam82

  committed
  1f4249d

  Copy full SHA for 1f4249d

• Use normal form characterization in nisErasable

  mattam82

  committed
  537e248

  Copy full SHA for 537e248

• Preservation of applications for proven for the whole pipeline

  mattam82

  committed
  84a264f

  Copy full SHA for 84a264f

• Cleanup ErasureCorrectness

  mattam82

  committed
  64b8171

  Copy full SHA for 64b8171

• Fix unqualified, ambiguous imports

  mattam82

  committed
  27d6ad2

  Copy full SHA for 27d6ad2

• Merge pull request #1013 from MetaCoq/compile-pipeline-app

  Show description for b63f41a
  mattam82

  authored
  b63f41a

  Copy full SHA for b63f41a

• separate extends and extends_eprogram

  tabareau

  committed
  b4ef021

  Copy full SHA for b4ef021

• prove missing lemmas of the pipeline

  tabareau

  committed
  3a954d5

  Copy full SHA for 3a954d5

• fix after rebase

  tabareau

  committed
  f941495

  Copy full SHA for f941495

• Merge pull request #1014 from MetaCoq/transform-extends-split

  Show description for 6eef155
  tabareau

  authored
  6eef155

  Copy full SHA for 6eef155

Commits on Nov 24, 2023

• Support primitive array terms

  mattam82

  committed
  4566665

  Copy full SHA for 4566665

• WIP up to confluence for arrays

  mattam82

  committed
  ed544ea

  Copy full SHA for ed544ea

• Alpha-conv and validity done

  mattam82

  committed
  c86a3a8

  Copy full SHA for c86a3a8

• Proved subject reduction for arrays

  mattam82

  committed
  26779c7

  Copy full SHA for 26779c7

• Adapted all of PCUIC to primitive arrays (and in general term containers in primitives)

  mattam82

  committed
  a7af745

  Copy full SHA for a7af745

• Done with template <-> PCUIC. Working on safe checker

  mattam82

  committed
  e93c39c

  Copy full SHA for e93c39c

• Update PCUICPosition to include arrays

  mattam82

  committed
  3ee01a3

  Copy full SHA for 3ee01a3

• Updatet SafeConversion to arrays

  mattam82

  committed
  67bba98

  Copy full SHA for 67bba98

• Typechecking of arrays

  mattam82

  committed
  51cb57d

  Copy full SHA for 51cb57d

• In erasure, must update solve_all to automate proofs

  mattam82

  committed
  69c1f05

  Copy full SHA for 69c1f05

• WIP in erasure of arrays

  mattam82

  committed
  8ecbd0e

  Copy full SHA for 8ecbd0e

• Adapt erasure for primitive arrays

  mattam82

  committed
  3354847

  Copy full SHA for 3354847

• Disable quotation module build

  mattam82

  committed
  8b4d7a9

  Copy full SHA for 8b4d7a9

• Fixes after rebase

  mattam82

  committed
  133b5ad

  Copy full SHA for 133b5ad

Commits on Nov 27, 2023

• Adapted extraction correctness, only remaining wf_glob proofs

  mattam82

  committed
  2fc21e5

  Copy full SHA for 2fc21e5

Commits on Nov 28, 2023

• WIP on wellformedness proof

  mattam82

  committed
  5127430

  Copy full SHA for 5127430