| 1f6644e | Lennard Gäher | 08 September 2020, 16:00:06 UTC | SAT using UpToC | 11 September 2020, 13:44:43 UTC |
| b92d48d | Lennard Gäher | 08 September 2020, 15:26:44 UTC | useful uptoc analysis stuff | 11 September 2020, 13:44:40 UTC |
| c0ec6aa | Lennard Gäher | 03 September 2020, 18:16:50 UTC | refactoring, link coqdoc to non-flat versions of flat problems | 11 September 2020, 13:44:37 UTC |
| 8a1f410 | Lennard Gäher | 30 August 2020, 09:23:13 UTC | fix compilation | 11 September 2020, 13:42:54 UTC |
| 845d58f | Lennard Gäher | 22 August 2020, 21:04:16 UTC | various simplifications/minor changes | 11 September 2020, 13:42:33 UTC |
| 114b5d7 | Lennard Gäher | 05 August 2020, 07:37:29 UTC | re-introduce par; minor optimisation (only noticeable in interactive mode, not with coqc) | 31 August 2020, 08:12:57 UTC |
| 499864d | Lennard Gäher | 03 August 2020, 09:57:02 UTC | a bit of refactoring; remove par in uniqueness proof to significantly reduce RAM usage (takes 3.5GB instead of ~8GB at the cost of 21min instead of 17.5min wall time) | 31 August 2020, 08:12:57 UTC |
| c086246 | Lennard Gäher | 02 August 2020, 21:23:19 UTC | a bit of refactoring of tactics in TM to TPR translation, a few percent speedup | 31 August 2020, 08:12:57 UTC |
| 3db576b | Fabian Kunze | 01 August 2020, 01:09:57 UTC | Merge pull request #1 from lgaeher/coq-8.11 Merge TM to SAT part of Cook proof + Clique reduction + ... | 01 August 2020, 01:09:57 UTC |
| 8c47b45 | Fabian Kunze | 01 August 2020, 01:00:43 UTC | -Added CookLevin.v containing final lemma Merge branch 'coq-8.11' of github.com:lgaeher/coq-computability-complexity into coq-8.11-for-merge | 01 August 2020, 01:00:43 UTC |
| 84d067c | Fabian Kunze | 01 August 2020, 00:03:46 UTC | -improved Performance of Tm to TPR reduction by: *adding many manual inversion lemmas *adding "par:" selector for parallel ltac evaluation *added many "abstract" tacticals for work-heavy parts (does this save time? not sure) -also Merge branch 'coq-8.11' of github.com:lgaeher/coq-computability-complexity into coq-8.11-for-merge | 01 August 2020, 00:03:46 UTC |
| 0073adc | Lennard Gäher | 31 July 2020, 20:22:47 UTC | whoops, forgot to git add CoqProject | 31 July 2020, 20:22:47 UTC |
| fa56117 | Lennard Gäher | 31 July 2020, 20:21:38 UTC | move files to CookPrelim | 31 July 2020, 20:21:38 UTC |
| b7e1835 | Lennard Gäher | 31 July 2020, 20:03:57 UTC | remove won't-fix lemma in overview | 31 July 2020, 20:03:57 UTC |
| 9973368 | Lennard Gäher | 31 July 2020, 20:03:18 UTC | fix admitted stuff in TMflatComp | 31 July 2020, 20:03:18 UTC |
| ea335c1 | Fabian Kunze | 31 July 2020, 08:27:43 UTC | small tweaks to maybe speed up TM-to-TPR-reduction by decrasing backtracking | 31 July 2020, 08:27:43 UTC |
| 86c90b8 | Fabian Kunze | 31 July 2020, 08:27:12 UTC | Additions for Cook-Levin Theorem | 31 July 2020, 08:27:12 UTC |
| 6c40be2 | Lennard Gäher | 30 July 2020, 21:08:04 UTC | remove LLNat + LLists + merge into other files; fix compilation; TODOs: two admitteds in L/TM/TMFlatComp; overview.v | 30 July 2020, 21:08:04 UTC |
| af880f5 | Fabian Kunze | 24 July 2020, 09:52:59 UTC | -added install script instructions for dependencies -adjusted TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP to be slightly more general, allowing it to connect to the other halve of the proof | 24 July 2020, 09:52:59 UTC |
| 8d6e95b | Lennard Gäher | 23 July 2020, 21:46:05 UTC | remove experimental UpToCNary poly file | 23 July 2020, 21:46:05 UTC |
| 533d505 | Lennard Gäher | 23 July 2020, 21:43:22 UTC | restore website gitignore | 23 July 2020, 21:43:22 UTC |
| 85c6ab8 | Lennard Gäher | 23 July 2020, 19:45:23 UTC | remove website config | 23 July 2020, 19:45:23 UTC |
| 57578cd | Lennard Gäher | 23 July 2020, 19:41:06 UTC | restore README.md to original | 23 July 2020, 19:41:06 UTC |
| 943cbd0 | Lennard Gäher | 23 July 2020, 19:40:19 UTC | remove website stuff | 23 July 2020, 19:40:19 UTC |
| d4d20c9 | Lennard Gäher | 23 July 2020, 19:38:39 UTC | remove tex stuff, SharpP | 23 July 2020, 19:38:39 UTC |
| f651de5 | Lennard Gäher | 23 July 2020, 17:50:44 UTC | fix all admitted goals that arose when porting | 23 July 2020, 17:50:44 UTC |
| 5e66486 | Lennard Gäher | 23 July 2020, 15:26:59 UTC | fix compilation under 8.11 | 23 July 2020, 15:27:19 UTC |
| 1b3691a | Lennard Gäher | 22 July 2020, 15:53:56 UTC | Merge remote-tracking branch 'origin/coq-8.11' into coq-8.11-2 | 22 July 2020, 15:53:56 UTC |
| bdf27d5 | Lennard Gäher | 22 July 2020, 15:43:44 UTC | continue work on port to 8.11 | 22 July 2020, 15:43:44 UTC |
| ac848af | Lennard Gäher | 22 July 2020, 15:42:38 UTC | minor fix to make leq_crossout work again | 22 July 2020, 15:42:38 UTC |
| 948e0fe | Fabian Kunze | 22 July 2020, 14:44:56 UTC | small tweaks | 22 July 2020, 14:44:56 UTC |
| f8d7c7d | Fabian Kunze | 22 July 2020, 10:57:25 UTC | Updated to new, ocally installed metacoq (see install.txt), allowing use of qualified names in extraction. Alsu added missing file | 22 July 2020, 10:57:25 UTC |
| 6292782 | Fabian Kunze | 20 July 2020, 14:38:26 UTC | tidies up a bit | 20 July 2020, 14:38:26 UTC |
| 9ae49c1 | Fabian Kunze | 15 July 2020, 12:17:13 UTC | finished reduction from gen-NP to gen-TM Left: small discrepancy in how the TM-alphabet is encoded | 15 July 2020, 12:57:00 UTC |
| 389e85e | Fabian Kunze | 08 July 2020, 13:43:15 UTC | continuation polyTimeComputability | 08 July 2020, 13:43:15 UTC |
| 3e3b665 | Fabian Kunze | 08 June 2020, 09:59:28 UTC | Finished non-computability-related part of LM to mTM reduction | 08 June 2020, 10:01:26 UTC |
| a9f3939 | Lennard Gäher | 06 June 2020, 21:36:45 UTC | Merge branch 'master' into coq-8.11-2 | 06 June 2020, 21:37:43 UTC |
| 0436312 | Lennard Gäher | 06 June 2020, 21:31:01 UTC | track changes | 06 June 2020, 21:31:01 UTC |
| f95e2be | Fabian Kunze | 04 June 2020, 13:05:18 UTC | WIP on LM to TM for closing Cook-Theorem-Assumptions | 04 June 2020, 13:05:18 UTC |
| 28e91e3 | Fabian Kunze | 26 May 2020, 10:28:32 UTC | -fixed "halt-or-diverge" definition for TMs -worked on LM->TM lemma | 26 May 2020, 10:28:32 UTC |
| 13f5bf7 | Fabian Kunze | 26 May 2020, 08:06:52 UTC | Completed construction of TM tfor LM->TM reduction | 26 May 2020, 08:06:52 UTC |
| d571df2 | Fabian Kunze | 08 May 2020, 10:47:23 UTC | finished size-analysis of LM-interpreter | 08 May 2020, 10:47:23 UTC |
| fe07be4 | Fabian Kunze | 07 May 2020, 10:10:34 UTC | -correctness of TM nearly complete -added more towards step-analysis of LAM | 07 May 2020, 10:10:34 UTC |
| 0f71516 | Fabian Kunze | 23 April 2020, 08:05:14 UTC | Merge remote-tracking branch 'computability-public/coq-8.11' into coq-8.11 | 23 April 2020, 08:05:14 UTC |
| c389de7 | Yannick Forster | 21 April 2020, 15:17:09 UTC | Merge pull request #48 from fakusb/coq-8.11-comp-only Refactored changes from private complexity-development | 21 April 2020, 15:17:09 UTC |
| f4db3ff | Fabian Kunze | 21 April 2020, 12:33:15 UTC | reenabled unused-intro-pattern warnings by default as the TM-framework disables them for all files that import the tactic causing them | 21 April 2020, 12:33:15 UTC |
| 5e60394 | Yannick Forster | 21 April 2020, 10:58:33 UTC | No warnings left | 21 April 2020, 10:58:33 UTC |
| bf41863 | Fabian Kunze | 21 April 2020, 09:24:42 UTC | -removed unneeded files -changed compilation order for better utilization of multi-core compilation (start large, monolithic files early) | 21 April 2020, 09:24:42 UTC |
| b9e7ca6 | Fabian Kunze | 21 April 2020, 09:01:12 UTC | Merge branch 'coq-8.11-comp-only' into coq-8.11 | 21 April 2020, 09:01:12 UTC |
| bb747c7 | Fabian Kunze | 20 April 2020, 14:58:25 UTC | refactored changes from private complexity-development in TM and L-extraction/verification frameworks | 20 April 2020, 16:42:57 UTC |
| 0c5766f | Fabian Kunze | 20 April 2020, 15:34:06 UTC | moved vector_to_list to own file | 20 April 2020, 15:34:06 UTC |
| 6b4ea4b | Fabian Kunze | 20 April 2020, 14:13:41 UTC | Merge remote-tracking branch 'computability-public/coq-8.11' into coq-8.11 | 20 April 2020, 14:13:41 UTC |
| 1755828 | Fabian Kunze | 20 April 2020, 12:52:50 UTC | Adjusted versions of external libraries to be taken from opam again | 20 April 2020, 12:52:50 UTC |
| d717806 | Dominique Larchey-Wendling | 20 April 2020, 12:52:43 UTC | Merge pull request #47 from DmxLarchey/unify_Fin_pos Unify Fin.t / pos and Vector.t / vec | 20 April 2020, 12:52:43 UTC |
| 14775e7 | Dominique Larchey-Wendling | 20 April 2020, 10:00:33 UTC | more cleanup in pos/vec | 20 April 2020, 10:00:33 UTC |
| 83ca25b | Dominique Larchey-Wendling | 19 April 2020, 16:08:37 UTC | unified Vector.t and vec ... several problems. 1) vec_cons can no longer be used as a constructor but the notation _ ## _ can largely mitigate 2) Vector.cons X x n v = vec_cons X n x v ie the arguments are no in the same order. Ie when invoquing induction we explicit intro pattern, you need to rearrange arguments 3) default parameter names are diffents, typical v is replaced by t which means scripts that use autogenerated names will likely fail ... | 19 April 2020, 16:08:37 UTC |
| 968ddf4 | Dominique Larchey-Wendling | 19 April 2020, 14:46:48 UTC | Unified Fin.t and pos so that they are now identical instead of just isomorphic | 19 April 2020, 14:46:48 UTC |
| af569e5 | Fabian Kunze | 17 April 2020, 13:37:46 UTC | Merge remote-tracking branch 'computability-public/coq-8.11' into coq-8.11 | 17 April 2020, 13:38:18 UTC |
| 7ffb6a8 | Yannick Forster | 15 April 2020, 10:37:57 UTC | Merge pull request #43 from yforster/remove_more_warnings Remove more warnings in L and TM | 15 April 2020, 10:37:57 UTC |
| c3931b6 | Dominique Larchey-Wendling | 15 April 2020, 09:36:24 UTC | removed unnecessary Checks in library files | 15 April 2020, 09:36:24 UTC |
| fff92d4 | Fabian Kunze | 15 April 2020, 08:38:56 UTC | Merge commit 'b9b3834' into coq-8.10 | 15 April 2020, 08:38:56 UTC |
| 94522db | Yannick Forster | 15 April 2020, 08:34:35 UTC | Remove last warnings, remove more printing | 15 April 2020, 08:34:35 UTC |
| a6d4b06 | Yannick Forster | 25 March 2020, 08:20:05 UTC | Removed submodules and updated opam file | 15 April 2020, 08:34:07 UTC |
| 67b68e6 | Yannick Forster | 15 April 2020, 07:01:21 UTC | remove more printing | 15 April 2020, 07:01:21 UTC |
| 455aa7a | Dominique Larchey-Wendling | 14 April 2020, 23:50:18 UTC | forgot to update bool_list.v and seqeq.v | 14 April 2020, 23:50:18 UTC |
| 2d1088e | Dominique Larchey-Wendling | 14 April 2020, 21:41:28 UTC | update Shared/Libs/DLW for ": core" hints warnings | 14 April 2020, 21:41:28 UTC |
| 26cb31b | Yannick Forster | 14 April 2020, 17:01:26 UTC | Remove last warnings | 14 April 2020, 17:01:26 UTC |
| 383a144 | Yannick Forster | 14 April 2020, 16:38:37 UTC | Remove lots of warnings in L and TM parts | 14 April 2020, 16:38:37 UTC |
| 3ad4cb8 | Yannick Forster | 14 April 2020, 13:00:29 UTC | fix opam repo add | 14 April 2020, 13:00:33 UTC |
| 64ecf83 | Yannick Forster | 14 April 2020, 08:07:40 UTC | Update License | 14 April 2020, 13:00:33 UTC |
| e7a7d52 | Yannick Forster | 14 April 2020, 08:06:48 UTC | Update README | 14 April 2020, 13:00:33 UTC |
| af4263c | Yannick Forster | 14 April 2020, 12:59:16 UTC | Merge pull request #40 from mrhaandi/coq-8.11-nowarn Less Warnings, Improved Compilation Speed | 14 April 2020, 12:59:16 UTC |
| 44c839e | mrhaandi | 14 April 2020, 11:54:16 UTC | merged TRAKHTENBROT from upstream | 14 April 2020, 11:54:16 UTC |
| bf25a30 | Yannick Forster | 14 April 2020, 10:49:40 UTC | Merge pull request #41 from DmxLarchey/trakhtenbrot Proposal to integrate the Trakhtenbrot code (IJCAR 2020) | 14 April 2020, 10:49:40 UTC |
| 33bb80d | Dominique Larchey-Wendling | 13 April 2020, 17:30:55 UTC | Dispatched Problems/PCP.v into PCP/PCP.c PCP/Reductions/*_iff*.v | 13 April 2020, 17:30:55 UTC |
| bc33a60 | Dominique Larchey-Wendling | 13 April 2020, 09:35:56 UTC | informativelly_reduces | 13 April 2020, 09:35:56 UTC |
| 09c23a9 | Dominique Larchey-Wendling | 11 April 2020, 21:24:44 UTC | Merge pull request #10 from DmxLarchey/ij1 integrated the TRAKHTENBROT code with informative reductions | 11 April 2020, 21:24:44 UTC |
| 131ba49 | Dominique Larchey-Wendling | 11 April 2020, 21:22:23 UTC | integrated the TRAKHTENBROT code with informative reductions | 11 April 2020, 21:22:23 UTC |
| f1bde74 | Dominique Larchey-Wendling | 11 April 2020, 20:46:05 UTC | Merge pull request #9 from DmxLarchey/ij1 merging Problems/*.v and Shared/Prelims.v for the Trakhtenbrot devel | 11 April 2020, 20:46:05 UTC |
| aed0a05 | Dominique Larchey-Wendling | 11 April 2020, 20:44:34 UTC | informative and non-informative reductions | 11 April 2020, 20:44:34 UTC |
| 237ea69 | Dominique Larchey-Wendling | 11 April 2020, 20:18:10 UTC | merging Problems/*.v and Shared/Prelims.v for the Trakhtenbrot devel | 11 April 2020, 20:18:10 UTC |
| 29b03ef | Dominique Larchey-Wendling | 11 April 2020, 20:10:02 UTC | Merge pull request #8 from DmxLarchey/ij1 Merge libs from trakhtenbrot | 11 April 2020, 20:10:02 UTC |
| 13c9b20 | Dominique Larchey-Wendling | 11 April 2020, 20:03:21 UTC | removed one cutrewrite | 11 April 2020, 20:03:21 UTC |
| 3b184e1 | Dominique Larchey-Wendling | 11 April 2020, 19:53:18 UTC | reverted orig libs | 11 April 2020, 19:53:18 UTC |
| 109cbb7 | Dominique Larchey-Wendling | 11 April 2020, 19:44:16 UTC | Revert "Delete vec.v" This reverts commit 1991a25ab6b82f256292db63ce90100454f212c7. | 11 April 2020, 19:44:16 UTC |
| 1991a25 | Dominique Larchey-Wendling | 11 April 2020, 19:38:32 UTC | Delete vec.v | 11 April 2020, 19:38:32 UTC |
| 6cbf46e | Dominique Larchey-Wendling | 11 April 2020, 19:29:10 UTC | to compare with the IJCAR lib | 11 April 2020, 19:29:10 UTC |
| 645aeb1 | Dominique Larchey-Wendling | 11 April 2020, 19:02:34 UTC | removed warnings | 11 April 2020, 19:02:34 UTC |
| ec2650d | Dominique Larchey-Wendling | 11 April 2020, 09:14:19 UTC | Merge pull request #5 from DmxLarchey/libs_update Libs update | 11 April 2020, 09:14:19 UTC |
| a3f8fee | mrhaandi | 10 April 2020, 18:14:31 UTC | replaced cutrewrite (x = y) by replace x with y | 10 April 2020, 18:14:31 UTC |
| f7f3190 | mrhaandi | 10 April 2020, 17:57:08 UTC | removed some minor warnings | 10 April 2020, 17:57:08 UTC |
| e1baf70 | mrhaandi | 10 April 2020, 17:39:31 UTC | small LAM and TM warning fixes | 10 April 2020, 17:39:31 UTC |
| 3b034e5 | mrhaandi | 10 April 2020, 17:05:02 UTC | dealt with warnings in HOU | 10 April 2020, 17:05:02 UTC |
| 365a80b | mrhaandi | 10 April 2020, 16:41:18 UTC | dealt with ILL warnings | 10 April 2020, 16:41:18 UTC |
| edae7bf | mrhaandi | 10 April 2020, 15:24:48 UTC | dealt with warnings in MuRec | 10 April 2020, 15:24:48 UTC |
| 08f37e5 | mrhaandi | 10 April 2020, 14:58:44 UTC | dealt with warnings in H10 | 10 April 2020, 14:58:44 UTC |
| d21270a | mrhaandi | 10 April 2020, 13:30:03 UTC | no warnings in MM | 10 April 2020, 13:30:03 UTC |
| 8fb7469 | mrhaandi | 10 April 2020, 12:29:56 UTC | improved PCP, CFG, SR compilation speed eliminated PCP, CFG, SR compilation warnings removed several Print Assumptions, improving compilation speed | 10 April 2020, 12:29:56 UTC |
| 12848be | Yannick Forster | 09 April 2020, 14:47:13 UTC | Update README.md | 09 April 2020, 14:47:13 UTC |
| 4a55a78 | Yannick Forster | 09 April 2020, 14:35:58 UTC | Update README.md | 09 April 2020, 14:35:58 UTC |
