| e24a92a | Fabian Kunze | 03 February 2021, 23:29:51 UTC | added missing html doc | 03 February 2021, 23:29:51 UTC |
| 6e9ec7e | Fabian Kunze | 03 February 2021, 15:10:33 UTC | Set theme jekyll-theme-slate | 03 February 2021, 15:10:33 UTC |
| e7c7c69 | Fabian Kunze | 03 February 2021, 15:06:28 UTC | doc compiled | 03 February 2021, 15:06:28 UTC |
| 59c2e0f | Fabian Kunze | 03 February 2021, 15:05:53 UTC | Merge branch 'paper-cook-levin' of github.com:uds-psl/cook-levin into paper-cook-levin | 03 February 2021, 15:05:53 UTC |
| 20c84fb | Fabian Kunze | 03 February 2021, 15:05:27 UTC | seperated out NP-containment of SAT | 03 February 2021, 15:05:27 UTC |
| 261e578 | Fabian Kunze | 02 February 2021, 13:36:13 UTC | Update README.md | 02 February 2021, 13:36:13 UTC |
| 50a378a | Fabian Kunze | 02 February 2021, 13:35:57 UTC | Update README.md | 02 February 2021, 13:35:57 UTC |
| 7a0b66f | Fabian Kunze | 02 February 2021, 13:34:56 UTC | Update README.md | 02 February 2021, 13:34:56 UTC |
| 602ee97 | Fabian Kunze | 02 February 2021, 13:34:27 UTC | Update README.md added more install instructions | 02 February 2021, 13:34:27 UTC |
| e047807 | Fabian Kunze | 02 February 2021, 13:32:16 UTC | Update build.yml added external repo | 02 February 2021, 13:32:16 UTC |
| e1be020 | Fabian Kunze | 02 February 2021, 13:24:21 UTC | Update README.md coq version | 02 February 2021, 13:24:21 UTC |
| ee04078 | Fabian Kunze | 01 February 2021, 11:08:31 UTC | rebuild doc | 01 February 2021, 11:08:31 UTC |
| 93f57c3 | Fabian Kunze | 01 February 2021, 10:51:57 UTC | fixed rendering of proof using | 01 February 2021, 10:51:57 UTC |
| 453e42b | lgaeher | 31 January 2021, 21:34:00 UTC | Update README.md | 31 January 2021, 21:34:00 UTC |
| 545e68a | Lennard Gäher | 31 January 2021, 21:23:11 UTC | hopefully fix build | 31 January 2021, 21:23:11 UTC |
| aba9dd6 | Fabian Kunze | 29 January 2021, 13:56:23 UTC | Merge branch 'paper-cook-levin' of github.com:uds-psl/cook-levin into paper-cook-levin | 29 January 2021, 13:56:23 UTC |
| 685dadf | Fabian Kunze | 29 January 2021, 13:55:59 UTC | small tweak to not have "P = NP" rendered in HTML doc | 29 January 2021, 13:55:59 UTC |
| e69eecd | Lennard Gäher | 29 January 2021, 12:20:11 UTC | line count script | 29 January 2021, 12:20:11 UTC |
| f72222a | Fabian Kunze | 29 January 2021, 11:54:10 UTC | Merge branch 'coq-8.12' into paper-cook-levin | 29 January 2021, 11:54:10 UTC |
| f4f7088 | Fabian Kunze | 29 January 2021, 11:49:37 UTC | adjusted entry point for coqdoc | 29 January 2021, 11:51:04 UTC |
| 97eb8ae | Fabian Kunze | 29 January 2021, 11:45:33 UTC | adjusted submodule url | 29 January 2021, 11:45:33 UTC |
| 5782a6a | Fabian Kunze | 29 January 2021, 11:39:09 UTC | CI | 29 January 2021, 11:39:09 UTC |
| 48ee39e | Fabian Kunze | 29 January 2021, 11:29:41 UTC | -adjusted Makefile to always use submodule, and allow `make html` to update coqdoc -added coqdoc and readme | 29 January 2021, 11:29:41 UTC |
| 6874967 | Lennard Gäher | 29 January 2021, 10:17:35 UTC | Merge branch 'cleanupCookLevin' of https://github.com/uds-psl/coq-library-complexity into cleanupCookLevin | 29 January 2021, 10:17:35 UTC |
| 08a04f6 | Lennard Gäher | 29 January 2021, 10:17:32 UTC | cleanup the comparison for time bound derivation, remove the polyTimeComputable approach from the comparison | 29 January 2021, 10:17:32 UTC |
| 887e0fa | lgaeher | 28 January 2021, 17:40:48 UTC | Update README.md | 28 January 2021, 17:40:48 UTC |
| fb5af28 | Fabian Kunze | 26 January 2021, 19:46:41 UTC | small renamings | 26 January 2021, 19:46:41 UTC |
| 8a40c1e | Fabian Kunze | 25 January 2021, 13:49:22 UTC | -partial work towards using a compiler for reduction from L to TM in one step -some simplifications for cook-levin paper | 25 January 2021, 13:49:22 UTC |
| bc20a70 | Fabian Kunze | 06 December 2020, 14:37:51 UTC | updates to more recent undec-lib-version | 06 December 2020, 14:37:51 UTC |
| 2646628 | Fabian Kunze | 05 December 2020, 14:22:48 UTC | added "Proof." where it as missing | 05 December 2020, 14:22:48 UTC |
| 970f2fe | Fabian Kunze | 04 December 2020, 20:29:58 UTC | removed unnecessary "Defined" | 04 December 2020, 20:29:58 UTC |
| f87234f | Fabian Kunze | 04 December 2020, 19:49:05 UTC | incorperated the "proof using type"s from undec | 04 December 2020, 19:49:05 UTC |
| 50a2ec6 | Fabian Kunze | 01 December 2020, 14:34:49 UTC | Reorganised file structure | 01 December 2020, 21:31:16 UTC |
| b90b32e | Fabian Kunze | 01 December 2020, 14:34:49 UTC | cleanup in checkDecodeBoolList | 01 December 2020, 14:35:53 UTC |
| c40e7be | Fabian Kunze | 27 November 2020, 14:46:48 UTC | -removed the specialisation of complexity definitions to sigma types -integrated neecessary changes to unde clibrary to allow encodability of sig-types | 27 November 2020, 14:54:49 UTC |
| 8c6fb9d | Fabian Kunze | 26 November 2020, 11:48:38 UTC | Improved build time (#10) -Improved build time of TM-to-TCC reduction -removed all warnings -made compatible with newest changes in undec-library | 26 November 2020, 11:48:38 UTC |
| 9f98aeb | Fabian Kunze | 20 November 2020, 09:19:41 UTC | typos | 20 November 2020, 09:19:41 UTC |
| 24aeac1 | Fabian Kunze | 20 November 2020, 07:27:44 UTC | enabled dual mode for build, either via submodule or via opam, which … (#9) * enabled dual mode for build, either via submodule or via opam, which enables ci-caching and convenient development on local machine | 20 November 2020, 07:27:44 UTC |
| 337964a | Fabian Kunze | 19 November 2020, 00:39:03 UTC | remove base library dependency | 19 November 2020, 00:39:03 UTC |
| 5a9a8b4 | Fabian Kunze | 19 November 2020, 00:29:08 UTC | remove travis | 19 November 2020, 00:29:08 UTC |
| cdee5b3 | Fabian Kunze | 18 November 2020, 22:46:34 UTC | -rearranged build setup to use submodule, to always make clear which version of the undec-library is compatible with this repo -incorperated changes from undec-lib | 19 November 2020, 00:10:08 UTC |
| 39492ee | Fabian Kunze | 18 November 2020, 20:41:42 UTC | Merge branch 'coq-8.12' of github.com:uds-psl/coq-library-complexity into coq-8.12 | 18 November 2020, 20:41:42 UTC |
| 19fd160 | Fabian Kunze | 18 November 2020, 20:40:47 UTC | wip | 18 November 2020, 20:40:47 UTC |
| a0a2c16 | Fabian Kunze | 08 November 2020, 23:09:21 UTC | Update .travis.yml | 08 November 2020, 23:09:21 UTC |
| ffa0a48 | Fabian Kunze | 08 November 2020, 23:08:57 UTC | Update .travis.yml | 08 November 2020, 23:08:57 UTC |
| 5bd3097 | Fabian Kunze | 08 November 2020, 22:20:34 UTC | Update build.yml (#7) * Update build.yml Made sure dependencies are cached and recomputed if the opam-file changes * Update build.yml * Update build.yml pull before cache * Update README.md | 08 November 2020, 22:20:34 UTC |
| e4f6637 | Fabian Kunze | 07 November 2020, 16:34:12 UTC | Added github CI (#6) * Added github CI * updated metacoq to match * travis ci for pushes only on master * github-ci only once on PR * removed tests&doc build of deps from ci | 07 November 2020, 16:34:12 UTC |
| 307d840 | Fabian Kunze | 22 October 2020, 08:10:15 UTC | added travis to readme | 22 October 2020, 08:10:15 UTC |
| 6803e84 | Fabian Kunze | 21 October 2020, 12:17:16 UTC | test speedup | 22 October 2020, 08:06:00 UTC |
| 1bc66bf | Fabian Kunze | 21 October 2020, 12:17:16 UTC | added more timings to slow proof | 21 October 2020, 12:18:29 UTC |
| ca841e9 | Fabian Kunze | 12 October 2020, 08:44:32 UTC | test what happens in travis with slow files at end | 21 October 2020, 11:39:06 UTC |
| 85cbc89 | Fabian Kunze | 10 October 2020, 16:17:53 UTC | fixed duplicate builds in parallel jobs | 21 October 2020, 11:39:06 UTC |
| 683b4c9 | Fabian Kunze | 10 October 2020, 14:10:08 UTC | reenabled 2 jobs for make | 21 October 2020, 11:39:06 UTC |
| 469f5c0 | Fabian Kunze | 10 October 2020, 13:26:15 UTC | tried more to get CI to work | 21 October 2020, 11:39:06 UTC |
| 5555089 | Fabian Kunze | 10 October 2020, 13:13:43 UTC | sliced time-intensive part of proof | 21 October 2020, 11:39:06 UTC |
| 7e311eb | Fabian Kunze | 10 October 2020, 12:33:56 UTC | moved down to 1 job for less ram usage | 21 October 2020, 11:39:06 UTC |
| cf09233 | Fabian Kunze | 10 October 2020, 11:26:58 UTC | changed how I limit ram for travis | 21 October 2020, 11:39:06 UTC |
| f7eff59 | Fabian Kunze | 10 October 2020, 09:21:40 UTC | typo | 21 October 2020, 11:39:06 UTC |
| 8a7e7f1 | Fabian Kunze | 10 October 2020, 09:19:53 UTC | Modified makefile to really compile slow file first | 21 October 2020, 11:39:06 UTC |
| e120d1e | Fabian Kunze | 09 October 2020, 19:55:09 UTC | adjusted proofs to use less memory | 21 October 2020, 11:39:06 UTC |
| 6ee7c6c | Fabian Kunze | 09 October 2020, 17:34:10 UTC | enabled timed builds on travis | 21 October 2020, 11:39:06 UTC |
| fa63ae9 | Fabian Kunze | 09 October 2020, 16:20:38 UTC | travis:enable a seperate stage for travis to build dependencies seperately | 21 October 2020, 11:39:06 UTC |
| febba4c | Yannick Forster | 07 October 2020, 12:36:05 UTC | add travis_wait for undec library installation | 21 October 2020, 11:39:06 UTC |
| 9369e20 | Yannick Forster | 07 October 2020, 11:41:28 UTC | add travis file | 21 October 2020, 11:39:06 UTC |
| 095a75c | Fabian Kunze | 09 October 2020, 15:55:45 UTC | Compiles with upstream undec-lib again | 09 October 2020, 15:55:45 UTC |
| 73fbfb1 | Fabian Kunze | 07 October 2020, 13:42:14 UTC | sdjusted to Undec-lib changes | 07 October 2020, 13:42:14 UTC |
| 05549c7 | Fabian Kunze | 02 October 2020, 17:12:32 UTC | Made this a stand-alone-project, using the library of undecidable problems as external dependency | 02 October 2020, 17:20:35 UTC |
| 2f8378b | Fabian Kunze | 02 October 2020, 11:52:00 UTC | Ported to coq 8.12, removed omega, removed warnings | 02 October 2020, 13:53:41 UTC |
| 18a7b02 | Fabian Kunze | 02 October 2020, 10:20:02 UTC | Merge commit '45a31a4d8da84f1afc2e99e72a87af4540472d8d' into coq-8.12 | 02 October 2020, 10:20:02 UTC |
| 755a3b3 | Fabian Kunze | 02 October 2020, 10:16:13 UTC | Merge commit '5581a0e0d80964cbbd0dbfdb84d7f6bc0e3d59e1' into coq-8.12 | 02 October 2020, 10:16:13 UTC |
| acf3525 | Fabian Kunze | 01 October 2020, 19:43:27 UTC | Merge remote-tracking branch 'computability-public/coq-8.11' into coq-8.11 | 01 October 2020, 19:43:27 UTC |
| 446c7d5 | Fabian Kunze | 01 October 2020, 19:42:31 UTC | Merge commit 'f4e599c' into coq-8.11 | 01 October 2020, 19:42:31 UTC |
| ca0bafa | Fabian Kunze | 29 September 2020, 12:52:08 UTC | merge 'bfa7788' into coq-8.11 | 29 September 2020, 14:01:09 UTC |
| e38547f | Fabian Kunze | 29 September 2020, 12:45:25 UTC | Merge commit '32c934d' into coq-8.11 | 29 September 2020, 12:45:25 UTC |
| 9ab15c6 | Lennard Gäher | 17 September 2020, 16:27:17 UTC | attempts at making polyTimeComputable work nicely, failing, see comments | 29 September 2020, 11:15:19 UTC |
| 529b97c | Lennard Gäher | 16 September 2020, 19:44:19 UTC | first version of bench file + remarks on how to go forward with polyTimeComputable | 29 September 2020, 11:15:19 UTC |
| 9f2dc99 | Lennard Gäher | 13 September 2020, 18:05:23 UTC | simplified sat verifier based on forallb/existsb | 29 September 2020, 11:15:19 UTC |
| 8af943f | Lennard Gäher | 12 September 2020, 17:04:17 UTC | simplify SAT verifier by removing the assignment_small requirement | 29 September 2020, 11:15:19 UTC |
| 064e118 | Lennard Gäher | 12 September 2020, 13:25:21 UTC | refactor PR related stuff, rename to CC | 29 September 2020, 11:15:19 UTC |
| 74c26a4 | Fabian Kunze | 11 September 2020, 13:33:32 UTC | renamed and moved around some files | 29 September 2020, 11:15:10 UTC |
| f9766c4 | Lennard Gäher | 10 September 2020, 17:36:57 UTC | merge overview.v and CookLevin.v into single file; move stuff around a bit | 29 September 2020, 10:20:37 UTC |
| 45a31a4 | Yannick Forster | 29 September 2020, 08:35:40 UTC | Merge pull request #61 from yforster/BinaryTMs Binary Turing machines and direct reduction from Turing machines to BSM | 29 September 2020, 08:35:40 UTC |
| 3d2beed | Lennard Gäher | 10 September 2020, 16:11:46 UTC | analysis of SAT verifier using UpToC | 11 September 2020, 13:44:46 UTC |
| 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 |
| bc9fb0d | Yannick Forster | 17 August 2020, 16:07:56 UTC | Merge pull request #60 from uds-psl/update-readme Branch for Coq 8.12 | 17 August 2020, 16:07:56 UTC |
| 537e027 | Yannick Forster | 17 August 2020, 16:07:41 UTC | Update README.md | 17 August 2020, 16:07:41 UTC |
| f078bf9 | Yannick Forster | 12 August 2020, 16:18:41 UTC | Finish Reduction SBTM -> BSM | 12 August 2020, 16:18:41 UTC |
| 1269694 | Yannick Forster | 07 August 2020, 14:30:00 UTC | Finish reduction | 07 August 2020, 14:30:14 UTC |
| 94630af | Yannick Forster | 07 August 2020, 10:18:58 UTC | save | 07 August 2020, 10:18:58 UTC |
| 713667d | Yannick Forster | 07 August 2020, 09:36:25 UTC | Progress | 07 August 2020, 09:36:25 UTC |
| 24b7774 | Yannick Forster | 07 August 2020, 07:10:49 UTC | Progress | 07 August 2020, 07:10:49 UTC |
| 7ec8a5a | Yannick Forster | 07 August 2020, 07:05:16 UTC | start binary TM compiler | 07 August 2020, 07:05:16 UTC |
| 977e917 | Yannick Forster | 04 August 2020, 14:56:05 UTC | Update README.md | 04 August 2020, 14:56:05 UTC |
