| ebcd89f | Matthieu Sozeau | 19 January 2021, 14:59:22 UTC | Merge pull request #540 from yforster/coq-8.12-jan18 Preparing for `coq-metacoq.1.0~beta2+8.12` | 19 January 2021, 14:59:22 UTC |
| ae198c3 | Yannick Forster | 18 January 2021, 11:31:20 UTC | fix compilation | 18 January 2021, 11:31:20 UTC |
| 85596d8 | Yannick Forster | 18 January 2021, 10:05:01 UTC | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12 | 18 January 2021, 10:05:01 UTC |
| 8d576c7 | Matthieu Sozeau | 04 January 2021, 09:30:58 UTC | Merge pull request #538 from jakobbotsch/eval-no-axioms Remove evaluation of axioms from wcbv and add proof of consistency using safe reduction + canonicity | 04 January 2021, 09:30:58 UTC |
| f1655e7 | Jakob Botsch Nielsen | 17 December 2020, 11:56:30 UTC | Add a proof of consistency using safe reduction and canonicity | 17 December 2020, 11:56:30 UTC |
| f0f58cc | Jakob Botsch Nielsen | 17 December 2020, 10:48:14 UTC | Remove wcbv evaluation of axioms in PCUIC In PCUIC we treated axioms as values, but we did not consistently treat eg. fixpoints and cases stuck on axioms as values. This removes the evaluation of axioms in PCUIC and gets rid of the axiom_free assumption that was needed for erasure because of it. | 17 December 2020, 10:49:30 UTC |
| 753ac0b | Matthieu Sozeau | 15 December 2020, 09:57:31 UTC | Fix update_plugin for OSX (bad sed was used there) | 15 December 2020, 17:17:00 UTC |
| eac7ac6 | Matthieu Sozeau | 15 December 2020, 17:11:36 UTC | Fix universe problem due to (stronger) minimization heursitic | 15 December 2020, 17:15:50 UTC |
| 30d7b72 | Matthieu Sozeau | 15 December 2020, 09:48:27 UTC | Merge pull request #536 from yforster/8.11_into_8.12 Merge again 8.11 into 8.12 | 15 December 2020, 09:48:27 UTC |
| f1820f9 | Yannick Forster | 14 December 2020, 21:02:21 UTC | trigger ci | 14 December 2020, 21:02:21 UTC |
| e3866e1 | Yannick Forster | 14 December 2020, 13:08:38 UTC | fix merge | 14 December 2020, 13:08:38 UTC |
| 170b4d1 | Yannick Forster | 14 December 2020, 11:58:04 UTC | Merge branch 'coq-8.11' into coq-8.12 | 14 December 2020, 11:58:04 UTC |
| 18d18e0 | Matthieu Sozeau | 13 December 2020, 00:33:36 UTC | Merge pull request #533 from MetaCoq/template-pcuic-proofs Template <-> PCUIC proofs | 13 December 2020, 00:33:36 UTC |
| 643424b | Matthieu Sozeau | 12 December 2020, 21:34:09 UTC | Remove test-suite relying on unproven checker | 12 December 2020, 21:34:09 UTC |
| 5b34d94 | Matthieu Sozeau | 12 December 2020, 16:02:23 UTC | Remove remaining references to checker/ | 12 December 2020, 16:21:49 UTC |
| ee6cc50 | Matthieu Sozeau | 12 December 2020, 11:52:59 UTC | TemplateToPCUIC proof | 12 December 2020, 11:52:59 UTC |
| 0352ad3 | Matthieu Sozeau | 12 December 2020, 11:23:16 UTC | Fix configure.sh | 12 December 2020, 11:23:16 UTC |
| f6e977d | Matthieu Sozeau | 12 December 2020, 03:24:09 UTC | Put the Checker in Template Coq as it can be used to play with reified terms | 12 December 2020, 03:37:05 UTC |
| f8ab08d | Matthieu Sozeau | 12 December 2020, 03:10:06 UTC | Really remove all references to the old checker | 12 December 2020, 03:14:43 UTC |
| 23b0060 | Matthieu Sozeau | 12 December 2020, 02:35:41 UTC | Fix compilation | 12 December 2020, 02:35:41 UTC |
| 2ec7fe1 | Matthieu Sozeau | 12 December 2020, 02:01:59 UTC | Cleaned up and documented PCUICToTemplateCorrectness | 12 December 2020, 02:08:17 UTC |
| f4b79ff | Matthieu Sozeau | 11 December 2020, 19:56:07 UTC | Finished PCUICToTemplate correctness proof.This is much less trivial than anticipated: one really has to do surgeryon the binary applications derivation to produce onewhere applications are n-ary *without* relying on transitivity of cumulativityanywhere. This requires to use induction on the size of derivations (includingnon-principal/paranoid hypotheses). | 12 December 2020, 01:27:00 UTC |
| f363cd4 | Matthieu Sozeau | 11 December 2020, 14:12:00 UTC | Remove entirely the checker folder, no longer needed | 11 December 2020, 14:48:46 UTC |
| f9d81e9 | Matthieu Sozeau | 11 December 2020, 13:46:56 UTC | Use strip_casts when checking fixpoints/cofixpoint types | 11 December 2020, 13:46:56 UTC |
| 903afe6 | Matthieu Sozeau | 10 December 2020, 11:08:34 UTC | Make PCUIC -> Template parametric on checker_flags | 10 December 2020, 11:08:34 UTC |
| 0500201 | Matthieu Sozeau | 10 December 2020, 11:01:59 UTC | Cleanup dependencies, PCUIC -> Template does not need substitution | 10 December 2020, 11:01:59 UTC |
| 3a5c31e | Matthieu Sozeau | 10 December 2020, 10:33:23 UTC | Merge pull request #531 from MetaCoq/primitive-int-float Primitive integers and floats | 10 December 2020, 10:33:23 UTC |
| 054a3d7 | Matthieu Sozeau | 10 December 2020, 09:54:14 UTC | Fix imports | 10 December 2020, 09:54:14 UTC |
| 80eb0fe | Matthieu Sozeau | 10 December 2020, 03:02:44 UTC | PCUIC -> Template relies on Substitution from the Checker | 10 December 2020, 03:02:44 UTC |
| bf81d71 | Matthieu Sozeau | 10 December 2020, 02:55:52 UTC | Move destArity to AstUtils | 10 December 2020, 02:55:52 UTC |
| 21e77a0 | Matthieu Sozeau | 10 December 2020, 02:09:04 UTC | Updating Template -> PCUIC | 10 December 2020, 02:41:13 UTC |
| 319a360 | Matthieu Sozeau | 10 December 2020, 01:09:20 UTC | Finished PCUIC -> Template proofs | 10 December 2020, 02:41:13 UTC |
| 14b1cb3 | Matthieu Sozeau | 09 December 2020, 20:48:15 UTC | Remove isLambda condition on fixpoint bodies | 10 December 2020, 02:41:13 UTC |
| 326ed83 | Matthieu Sozeau | 09 December 2020, 20:37:03 UTC | Before removing isLambda | 10 December 2020, 02:41:13 UTC |
| cb5aaeb | Matthieu Sozeau | 09 December 2020, 01:31:13 UTC | Template -> PCUIC -> Template proofs | 10 December 2020, 02:41:13 UTC |
| 40aea2f | Matthieu Sozeau | 09 December 2020, 00:13:30 UTC | Update Template-Coq's typing derivations to match PCUIC more closely | 10 December 2020, 02:41:13 UTC |
| aa097dd | Matthieu Sozeau | 10 December 2020, 02:40:20 UTC | Another weak type variable problem | 10 December 2020, 02:40:20 UTC |
| 0649aed | Matthieu Sozeau | 08 December 2020, 15:46:40 UTC | Slight refinement: in PCUIC, use a common tagged sum for all primitive types | 09 December 2020, 19:23:06 UTC |
| 52ee5de | Matthieu Sozeau | 08 December 2020, 13:00:09 UTC | WIP on primitive types | 08 December 2020, 13:00:09 UTC |
| 2f93367 | Matthieu Sozeau | 05 December 2020, 16:56:51 UTC | Fix constr_quoter and add test-suite file for primitives | 05 December 2020, 16:58:19 UTC |
| b60716a | Matthieu Sozeau | 05 December 2020, 12:38:46 UTC | Fix configure.sg conditional? | 05 December 2020, 12:38:46 UTC |
| aaf56aa | Matthieu Sozeau | 05 December 2020, 12:01:15 UTC | Fix translations | 05 December 2020, 12:01:15 UTC |
| 6a13d55 | Matthieu Sozeau | 05 December 2020, 11:02:27 UTC | Fix Imports for opam installation | 05 December 2020, 11:02:27 UTC |
| 0858b8a | Matthieu Sozeau | 04 December 2020, 20:50:22 UTC | Move erasure to new ast as well (using model still) | 04 December 2020, 21:51:33 UTC |
| ffce387 | Matthieu Sozeau | 04 December 2020, 15:51:23 UTC | Add (modeled) ints and floats to PCUIC | 04 December 2020, 19:07:58 UTC |
| d71b2a0 | Matthieu Sozeau | 04 December 2020, 13:15:27 UTC | Fix Typing and cleanup | 04 December 2020, 13:15:27 UTC |
| f36c75d | Matthieu Sozeau | 04 December 2020, 12:18:37 UTC | Extract float64 as well | 04 December 2020, 12:48:56 UTC |
| a44cad1 | Matthieu Sozeau | 04 December 2020, 11:31:17 UTC | Support for primitive types | 04 December 2020, 11:41:59 UTC |
| f713e10 | Matthieu Sozeau | 04 December 2020, 11:31:06 UTC | ML reification of primitive int/floats | 04 December 2020, 11:41:59 UTC |
| 453dc7d | Fabian Kunze | 04 December 2020, 11:29:17 UTC | wip | 04 December 2020, 11:41:59 UTC |
| 879ef1d | Fabian Kunze | 04 December 2020, 08:40:09 UTC | extraction in template-coq compiles | 04 December 2020, 11:41:51 UTC |
| 9831832 | Matthieu Sozeau | 04 December 2020, 08:52:23 UTC | Merge pull request #530 from MetaCoq/unquote-evars Implement denotation of evars, with special case for "fresh_evar_id" | 04 December 2020, 08:52:23 UTC |
| 3b0aaf5 | Matthieu Sozeau | 03 December 2020, 22:00:10 UTC | Merge pull request #529 from jakobbotsch/fix-case-predicate-type Add missing reduction for predicate types | 03 December 2020, 22:00:10 UTC |
| c7f8694 | Matthieu Sozeau | 03 December 2020, 21:12:50 UTC | Implement denotation of evars, with special case for "fresh_evar_id" | 03 December 2020, 21:50:28 UTC |
| a878034 | Matthieu Sozeau | 03 December 2020, 13:20:10 UTC | Merge pull request #528 from MetaCoq/metacoq-tour MetaCoq tour | 03 December 2020, 13:20:10 UTC |
| 006b4ab | Matthieu Sozeau | 03 December 2020, 10:49:53 UTC | Dependency on erasure missing | 03 December 2020, 11:41:50 UTC |
| faa62ac | Jakob Botsch Nielsen | 03 December 2020, 10:23:48 UTC | Add missing reduction for predicate types The safe checker was destructing the inferred type of predicates directly as an arity, which was not complete. It meant that the following example was not accepted by the safe checker: Definition WrappedType := Type. Definition WrappedNat : WrappedType := nat. Definition foo : nat := match 0 return WrappedNat with | 0 => 0 | S n => 0 end. To fix we now use reduction for the predicate type. | 03 December 2020, 10:28:47 UTC |
| 2f197b3 | Yannick Forster | 03 December 2020, 10:06:50 UTC | Build on Windows (#526) * Fix two line ending bugs to build on Windows * no backslashes * four backslashes * Enable parallel builds on Windows ("-j12" is not recognised by make.exe, we need "-j" "12") | 03 December 2020, 10:06:50 UTC |
| 08de88c | Matthieu Sozeau | 03 December 2020, 00:07:48 UTC | Merge pull request #524 from MetaCoq/cleanup-safechecker Cleanup safechecker | 03 December 2020, 00:07:48 UTC |
| ed2de98 | Matthieu Sozeau | 02 December 2020, 23:58:17 UTC | Erasure live test shortening using the monad | 02 December 2020, 23:59:42 UTC |
| 66da11a | Matthieu Sozeau | 02 December 2020, 23:57:17 UTC | MetaCoq tour | 02 December 2020, 23:57:17 UTC |
| 6d7e989 | Matthieu Sozeau | 02 December 2020, 23:22:50 UTC | Fix erasure plugin install | 02 December 2020, 23:22:50 UTC |
| e79f5f1 | Matthieu Sozeau | 02 December 2020, 20:14:19 UTC | Fix erasure plugin build | 02 December 2020, 20:21:59 UTC |
| 74084cd | Matthieu Sozeau | 02 December 2020, 20:09:45 UTC | Clean Erasure.v to use "todos" only for the ultimate definition for testing erasure. | 02 December 2020, 20:09:45 UTC |
| 49f9f73 | Matthieu Sozeau | 02 December 2020, 17:13:47 UTC | Fix pr_char_list in safechecker to not use Scanf.unescaped, and add back fixing of universes, still needed in 8.11 | 02 December 2020, 17:13:47 UTC |
| a39dff3 | Matthieu Sozeau | 01 December 2020, 13:39:53 UTC | Some defs were blocking execution inside coq | 01 December 2020, 13:39:53 UTC |
| 9df4b96 | Matthieu Sozeau | 28 November 2020, 14:24:58 UTC | Decouple SafeChecker completely from erasure, at the ML level too | 28 November 2020, 14:24:58 UTC |
| ccb3882 | Matthieu Sozeau | 28 November 2020, 14:10:06 UTC | typing_correctness and erasure_live_test reducing again. | 28 November 2020, 14:10:06 UTC |
| b526cec | Matthieu Sozeau | 28 November 2020, 14:07:26 UTC | Finish decoupling of Type/SafeChecker and erasure: only retyping needed to compile it | 28 November 2020, 14:07:26 UTC |
| c27c0bb | Matthieu Sozeau | 27 November 2020, 22:46:21 UTC | Remove unnecessary depgraphs | 27 November 2020, 22:46:21 UTC |
| a54f1b5 | Matthieu Sozeau | 27 November 2020, 22:44:20 UTC | SafeConversion no longer needed | 27 November 2020, 22:44:20 UTC |
| 3c6db11 | Matthieu Sozeau | 27 November 2020, 22:00:41 UTC | Disable erasure_live_test for now | 27 November 2020, 22:00:41 UTC |
| 70c97dd | Matthieu Sozeau | 27 November 2020, 21:30:21 UTC | typing_correctness broken for now | 27 November 2020, 21:30:21 UTC |
| 27922a1 | Matthieu Sozeau | 27 November 2020, 21:09:19 UTC | Try to reduce coupling of files in safechecker and erasure | 27 November 2020, 21:22:01 UTC |
| 4d21fb3 | Matthieu Sozeau | 27 November 2020, 19:34:17 UTC | Bundle together the guard axioms in a class | 27 November 2020, 20:51:10 UTC |
| 4b52e65 | Matthieu Sozeau | 27 November 2020, 13:26:36 UTC | Split TypeChecker and Environment Checker, move auxilliary lemmas to their right place | 27 November 2020, 13:26:36 UTC |
| c46d77d | Matthieu Sozeau | 27 November 2020, 12:14:39 UTC | PCUICCumulativity no longer needed by erasure plugin | 27 November 2020, 12:14:39 UTC |
| 1aee3df | Matthieu Sozeau | 26 November 2020, 19:30:26 UTC | Flip app/app_inv naming for wf_local_rel/All_local_env/wf_local | 26 November 2020, 20:32:35 UTC |
| 2c0b4f0 | Matthieu Sozeau | 26 November 2020, 19:24:52 UTC | Rename wf_local_app -> wf_local_app_l | 26 November 2020, 20:32:35 UTC |
| 369e600 | Matthieu Sozeau | 26 November 2020, 19:19:48 UTC | WIP cleaning up | 26 November 2020, 20:32:35 UTC |
| 90669b3 | Matthieu Sozeau | 26 November 2020, 17:35:35 UTC | Fix due to move of conv_pb definition | 26 November 2020, 20:32:35 UTC |
| 6a0d029 | Matthieu Sozeau | 26 November 2020, 17:29:32 UTC | Dependency graph as of 2020-11-26 | 26 November 2020, 20:32:35 UTC |
| 5fcbe23 | Matthieu Sozeau | 26 November 2020, 17:29:05 UTC | Ignore notation-overridden warning temporarily | 26 November 2020, 20:32:35 UTC |
| 0516e48 | Matthieu Sozeau | 26 November 2020, 17:28:35 UTC | Adapt depgraph to Mac OS poor unix support | 26 November 2020, 20:32:35 UTC |
| 96778d1 | Matthieu Sozeau | 26 November 2020, 17:03:53 UTC | Remove distracting notation overriden warning | 26 November 2020, 20:32:35 UTC |
| 05be488 | Matthieu Sozeau | 26 November 2020, 14:04:30 UTC | Refactorings and cleanings- Used andb_and not to clash with ssrbool.andP- Move syntactic equality checking to a separate safechecker library- move monadic combinators to monad_utils | 26 November 2020, 20:32:35 UTC |
| a23b7c9 | Matthieu Sozeau | 26 November 2020, 18:46:04 UTC | Merge pull request #523 from MetaCoq/github-actions-8.11 Add GitHub actions workflow to 8.11 branch | 26 November 2020, 18:46:04 UTC |
| 273775f | Yannick Forster | 10 November 2020, 10:03:40 UTC | Add GitHub actions workflow Move to github action add local and opam build fix yml only local add ./configure.sh Update README.md | 26 November 2020, 16:41:08 UTC |
| 46c6867 | Matthieu Sozeau | 26 November 2020, 16:28:05 UTC | Fix Msg I messed up my previous fix, this should correct it. | 26 November 2020, 16:28:05 UTC |
| 165725a | Matthieu Sozeau | 26 November 2020, 16:26:40 UTC | Fix missing parenthesis | 26 November 2020, 16:26:40 UTC |
| 2c6e9ab | Matthieu Sozeau | 26 November 2020, 14:20:41 UTC | Merge pull request #522 from yforster/github_actions GitHub actions | 26 November 2020, 14:20:41 UTC |
| d9a9fac | Matthieu Sozeau | 26 November 2020, 13:30:33 UTC | Merge pull request #519 from MetaCoq/complete-safechecker Complete safechecker | 26 November 2020, 13:30:33 UTC |
| 1579a1a | Matthieu Sozeau | 26 November 2020, 11:36:34 UTC | Fixed empty error message | 26 November 2020, 11:36:34 UTC |
| c1beee7 | Matthieu Sozeau | 25 November 2020, 21:39:07 UTC | Remove unneded ml files | 25 November 2020, 21:39:07 UTC |
| ea89078 | Matthieu Sozeau | 25 November 2020, 18:20:35 UTC | Fixes after rebase | 25 November 2020, 20:20:02 UTC |
| d0b31fd | Matthieu Sozeau | 25 November 2020, 13:32:54 UTC | Complete positivity criterion, otherwise failure in safechecker_test | 25 November 2020, 18:13:46 UTC |
| 0503e6e | Matthieu Sozeau | 25 November 2020, 12:52:15 UTC | Finished checking except for projections | 25 November 2020, 18:13:46 UTC |
| c4790bf | Matthieu Sozeau | 25 November 2020, 01:22:27 UTC | Checking of constructors completed, projections remain | 25 November 2020, 18:13:46 UTC |
| d8dadf1 | Matthieu Sozeau | 23 November 2020, 21:55:08 UTC | Prove the ctx_inst obligation of on_constructor | 25 November 2020, 18:13:46 UTC |
| 653cdaa | Matthieu Sozeau | 22 November 2020, 19:22:38 UTC | Hit a nail in checking of constructors, need to refine constructor_shape | 25 November 2020, 18:10:50 UTC |
