| e38849f | Jason Gross | 28 June 2021, 20:45:50 UTC | Fix lingering xargs | 28 June 2021, 20:45:50 UTC |
| 0b1ebe1 | Jason Gross | 28 June 2021, 17:28:42 UTC | Fix perf.csv generation | 28 June 2021, 17:28:42 UTC |
| 1c8af8e | Jason Gross | 28 June 2021, 17:28:29 UTC | Don't invoke to_csv.py multiple times | 28 June 2021, 17:28:29 UTC |
| b0b15c5 | Jason Gross | 28 June 2021, 15:28:29 UTC | Update .gitignore | 28 June 2021, 15:28:29 UTC |
| 2d5fb85 | Jason Gross | 28 June 2021, 14:19:55 UTC | Add perf.csv | 28 June 2021, 14:29:14 UTC |
| 06f2828 | Jason Gross | 28 June 2021, 14:29:00 UTC | Add nlimbs column in perf.csv | 28 June 2021, 14:29:14 UTC |
| b463308 | Jason Gross | 28 June 2021, 14:10:06 UTC | Update file writing to avoid error make: execvp: /bin/sh: Argument list too long | 28 June 2021, 14:19:29 UTC |
| 7d82408 | Jason Gross | 11 November 2019, 19:55:44 UTC | Add perf data | 27 November 2019, 22:03:10 UTC |
| c1dd0ac | Jason Gross | 08 November 2019, 00:08:57 UTC | Update .gitignore, enable precomputation | 27 November 2019, 22:03:10 UTC |
| 75a06fc | Jason Gross | 27 November 2019, 22:02:38 UTC | Bump rewriter | 27 November 2019, 22:02:38 UTC |
| 905578f | Jason Gross | 27 November 2019, 19:13:43 UTC | Fix a typo | 27 November 2019, 19:13:43 UTC |
| 60f3718 | Jason Gross | 27 November 2019, 19:05:52 UTC | Quieter build | 27 November 2019, 19:05:52 UTC |
| 011f79a | Jason Gross | 27 November 2019, 19:00:10 UTC | Test output of some computations | 27 November 2019, 19:00:10 UTC |
| fecc72d | Jason Gross | 27 November 2019, 18:41:04 UTC | Bump rewriter | 27 November 2019, 18:41:04 UTC |
| 3690ade | Jason Gross | 27 November 2019, 18:17:41 UTC | Bump coqprime | 27 November 2019, 18:17:41 UTC |
| 1ed5ed1 | Jason Gross | 27 November 2019, 16:08:01 UTC | Bump rewriter | 27 November 2019, 16:08:01 UTC |
| 23fe23d | Jason Gross | 27 November 2019, 15:12:07 UTC | Bump rewriter | 27 November 2019, 15:12:07 UTC |
| 10a1f47 | Jason Gross | 26 November 2019, 18:35:49 UTC | Bump rewriter | 26 November 2019, 18:35:49 UTC |
| 751cfb3 | Jason Gross | 26 November 2019, 04:25:44 UTC | Bump bedrock2 | 26 November 2019, 04:25:44 UTC |
| 9a86043 | Jason Gross | 26 November 2019, 04:23:26 UTC | Ignore *.vok | 26 November 2019, 04:23:26 UTC |
| 5c28ca0 | Jason Gross | 26 November 2019, 04:22:11 UTC | Bump bedrock | 26 November 2019, 04:22:11 UTC |
| 6ae1d84 | Jason Gross | 25 November 2019, 01:11:46 UTC | Update rewriter | 25 November 2019, 01:11:46 UTC |
| 144d4c5 | Jason Gross | 19 November 2019, 03:26:25 UTC | Bump rewriter | 19 November 2019, 03:26:25 UTC |
| 7e557e5 | Jason Gross | 19 November 2019, 02:50:54 UTC | Bump rewriter | 19 November 2019, 02:50:54 UTC |
| b5670d0 | Jason Gross | 15 November 2019, 09:13:02 UTC | Limit virtual memory rather than RSS apparently ulimit -m doesn't work anymore https://superuser.com/a/1497437/59575 / https://thirld.com/blog/2012/02/09/things-to-remember-when-using-ulimit/ | 19 November 2019, 02:43:15 UTC |
| 66a8016 | Jason Gross | 19 November 2019, 02:42:04 UTC | Remove package-rewriter.sh It's outdated | 19 November 2019, 02:42:31 UTC |
| 5f96a13 | Jason Gross | 19 November 2019, 01:10:30 UTC | Also build standalone-ocaml by default | 19 November 2019, 01:10:30 UTC |
| 5a0bee2 | Jason Gross | 15 November 2019, 06:12:11 UTC | Switch to ulimit for mem management | 15 November 2019, 06:12:11 UTC |
| 5166ca4 | Jason Gross | 15 November 2019, 05:59:18 UTC | Bump rewriter | 15 November 2019, 05:59:18 UTC |
| 837a33c | Jason Gross | 15 November 2019, 05:57:37 UTC | Switch to using cgroups for perf testing | 15 November 2019, 05:58:18 UTC |
| 2904d3a | Jason Gross | 14 November 2019, 23:01:00 UTC | Don't mem-limit perf-extraction; it's not a memory hog | 14 November 2019, 23:01:15 UTC |
| 8d6fa1d | Jason Gross | 13 November 2019, 19:09:44 UTC | Add perf-{except,only}-computed targets | 13 November 2019, 19:10:14 UTC |
| 7abc77a | Jason Gross | 12 November 2019, 08:08:44 UTC | Actually limit perf-testing to 10GB RAM | 12 November 2019, 08:09:27 UTC |
| 8c93d1f | Jason Gross | 12 November 2019, 08:06:32 UTC | Fix a typo | 12 November 2019, 08:06:52 UTC |
| 40d78d8 | Jason Gross | 12 November 2019, 07:48:36 UTC | Don't keep calling make.py on every invocation | 12 November 2019, 07:49:55 UTC |
| 9e4baf2 | Jason Gross | 11 November 2019, 19:57:24 UTC | Rearrange ordering of perf data to get more data that we care about | 11 November 2019, 19:57:24 UTC |
| dfd0366 | Jason Gross | 09 November 2019, 20:20:23 UTC | Don't remove native files after every build It was breaking parallel builds | 09 November 2019, 20:20:41 UTC |
| 93076eb | Jason Gross | 08 November 2019, 21:49:54 UTC | Be more compatible with coq/coq#11081 | 08 November 2019, 21:50:06 UTC |
| 5e94ad4 | Jason Gross | 08 November 2019, 19:19:53 UTC | Work around COQBUG(https://github.com/coq/coq/issues/10495) | 08 November 2019, 19:20:16 UTC |
| 984c34c | Jason Gross | 08 November 2019, 15:32:34 UTC | Stop using etc/timeout It seems to be breaking everything | 08 November 2019, 15:32:54 UTC |
| 6825be8 | Jason Gross | 08 November 2019, 06:07:30 UTC | Fix error reporting even with timeout No idea why the timeout script masks the output of the programs... | 08 November 2019, 06:08:29 UTC |
| 04ac001 | Jason Gross | 08 November 2019, 00:34:59 UTC | Use a more restrictive timeout command | 08 November 2019, 00:34:59 UTC |
| 6a1aba0 | Jason Gross | 08 November 2019, 00:29:38 UTC | Better handling of timeouts in perf | 08 November 2019, 00:29:38 UTC |
| 657f90d | Jason Gross | 08 November 2019, 00:13:13 UTC | Enable more stack space for larger perf | 08 November 2019, 00:13:13 UTC |
| 37dabab | Jason Gross | 07 November 2019, 23:38:50 UTC | Better memory limits on perf | 07 November 2019, 23:38:50 UTC |
| ddf8067 | Jason Gross | 07 November 2019, 23:37:05 UTC | Add timeout module for perf testing | 07 November 2019, 23:37:05 UTC |
| e9ac1af | Jason Gross | 07 November 2019, 23:31:24 UTC | Bump bedrock2 | 07 November 2019, 23:31:24 UTC |
| 24e8ad3 | Jason Gross | 07 November 2019, 23:30:10 UTC | Bump rewriter | 07 November 2019, 23:30:10 UTC |
| 0b6f6c8 | Jason Gross | 07 November 2019, 03:41:45 UTC | Bump rewriter | 07 November 2019, 03:41:45 UTC |
| 23a9053 | Jason Gross | 29 October 2019, 19:43:11 UTC | Fix a bunch of warnings and turn them into errors The build output is now a bit less noisy. | 07 November 2019, 02:59:28 UTC |
| cccdf93 | Jason Gross | 06 November 2019, 20:09:04 UTC | Fix an issue arising after bumping rewriter We changed the definition or prod_rect_nodep | 06 November 2019, 20:09:04 UTC |
| 3e197d2 | Jason Gross | 06 November 2019, 00:26:18 UTC | Bump rewriter | 06 November 2019, 00:26:18 UTC |
| 4eafec0 | Jason Gross | 05 November 2019, 19:40:08 UTC | Bump rewriter after coq/coq#8642 | 05 November 2019, 19:40:08 UTC |
| a1e6e1e | Vincent Laporte | 04 November 2019, 14:49:20 UTC | Update coqprime | 05 November 2019, 19:39:13 UTC |
| bf5fe56 | Jason Gross | 04 November 2019, 22:33:01 UTC | Update .gitignore after coq/coq#8642 | 04 November 2019, 22:33:01 UTC |
| e9feec0 | Jason Gross | 04 November 2019, 21:12:43 UTC | Bump bedrock2 | 04 November 2019, 21:12:43 UTC |
| 5d8afb1 | Jason Gross | 04 November 2019, 19:48:20 UTC | Bump coq-scripts | 04 November 2019, 19:48:20 UTC |
| ab9b970 | Jason Gross | 02 November 2019, 05:44:12 UTC | Bump rewriter | 02 November 2019, 05:44:12 UTC |
| 5a51b7a | Jason Gross | 01 November 2019, 19:43:35 UTC | Update perf script to generate more txt files | 01 November 2019, 19:50:07 UTC |
| aef73bb | Jason Gross | 31 October 2019, 22:45:59 UTC | Also use git status on travis | 31 October 2019, 22:45:59 UTC |
| 11667b2 | Jason Gross | 31 October 2019, 22:44:57 UTC | Fix coqprime build to not remake the makefile | 31 October 2019, 22:44:57 UTC |
| 5588aa4 | Jason Gross | 31 October 2019, 20:30:14 UTC | Bump coqprime for better travis build on master | 31 October 2019, 20:30:14 UTC |
| fae7d62 | Jason Gross | 31 October 2019, 19:20:41 UTC | Show more diffs before exiting | 31 October 2019, 19:20:41 UTC |
| ef4f19a | Jason Gross | 31 October 2019, 02:16:51 UTC | Slightly more general check_precomputed_enabled | 31 October 2019, 02:16:51 UTC |
| 690263f | Jason Gross | 31 October 2019, 01:46:56 UTC | Add an extra travis stage for deps of fiat-crypto | 31 October 2019, 01:46:56 UTC |
| 6cfcf78 | Jason Gross | 31 October 2019, 01:44:15 UTC | Remove two more slow files from lite | 31 October 2019, 01:44:15 UTC |
| 6e78a3a | Jason Gross | 30 October 2019, 23:46:26 UTC | Add another excluded file to the lite target (it was too slow) | 30 October 2019, 23:46:26 UTC |
| 414190b | Jason Gross | 29 October 2019, 18:30:12 UTC | Bump rewriter submodule | 29 October 2019, 18:30:12 UTC |
| b5774c7 | Jason Gross | 29 October 2019, 18:22:01 UTC | Fix a typo | 29 October 2019, 18:22:01 UTC |
| eba1443 | Jason Gross | 16 October 2019, 04:56:11 UTC | Factor rewriter into a submodule dependency | 22 October 2019, 20:43:44 UTC |
| c1e7595 | Jason Gross | 10 October 2019, 03:43:27 UTC | [travis] Also test Coq 8.10.0, now that it's out | 22 October 2019, 16:30:55 UTC |
| 6280af6 | jadep | 15 October 2019, 22:04:18 UTC | change compute to vm_compute as recommended by Jason | 16 October 2019, 19:24:55 UTC |
| c7f1a92 | jadep | 15 October 2019, 22:03:17 UTC | fix printouts in CompilerTest.v | 16 October 2019, 19:24:55 UTC |
| db6b560 | jadep | 11 October 2019, 20:37:50 UTC | change valid_expr to a computable fixpoint | 16 October 2019, 19:24:55 UTC |
| ee8e1e9 | jadep | 11 October 2019, 20:05:18 UTC | add separation logic, fix more naming, reorganize correctness lemma, and change inductive to fixpoint for result equivalence | 16 October 2019, 19:24:55 UTC |
| 81e05fb | jadep | 10 October 2019, 17:31:49 UTC | change names from of_ to translate_ (as per Andres's code review suggestion) | 16 October 2019, 19:24:55 UTC |
| cf71ab6 | jadep | 10 October 2019, 17:26:54 UTC | pass after code review: change names, add offset for address indexing, improve comments | 16 October 2019, 19:24:55 UTC |
| c79cc56 | jadep | 10 October 2019, 15:41:03 UTC | fix uint64/uint32 notation in CompilerTest.v | 16 October 2019, 19:24:55 UTC |
| 71e125e | jadep | 10 October 2019, 14:21:24 UTC | change var for type.arrow so output variable names can't depend on argument names | 16 October 2019, 19:24:55 UTC |
| 48ce883 | jadep | 08 October 2019, 18:47:34 UTC | remove now-unused cast-outside-of-range implementation | 16 October 2019, 19:24:55 UTC |
| 93883ef | jadep | 08 October 2019, 18:35:38 UTC | fix bedrock compiler after rebase and reprint tests | 16 October 2019, 19:24:55 UTC |
| d0fe500 | jadep | 07 October 2019, 19:27:32 UTC | remove debugging section from Compiler.v | 16 October 2019, 19:24:55 UTC |
| 8d4f9cd | jadep | 07 October 2019, 19:04:03 UTC | fix bedrock compiler to handle Language API changes -- reprint everything in CompilerTest | 16 October 2019, 19:24:55 UTC |
| bf964db | jadep | 27 September 2019, 16:02:34 UTC | add another test case for 32-bit (currently fails because there are 64-bit integers here for some reason) | 16 October 2019, 19:24:55 UTC |
| 4264273 | jadep | 26 September 2019, 17:42:52 UTC | add CompilerTest to _CoqProject | 16 October 2019, 19:24:55 UTC |
| bd45446 | jadep | 26 September 2019, 17:42:25 UTC | first stab at proofs | 16 October 2019, 19:24:55 UTC |
| 111dfeb | jadep | 26 September 2019, 13:13:28 UTC | add special add-get-carry and add-with-get-carry clauses so that we can set variables for intermediate values; improve formatting of output in CompilerTest | 16 October 2019, 19:24:55 UTC |
| 0f8200c | jadep | 24 September 2019, 19:00:00 UTC | fix word size check | 16 October 2019, 19:24:55 UTC |
| 16413c0 | jadep | 24 September 2019, 18:56:22 UTC | add test run of compiler on an example from SlowPrimeSynthesis.v | 16 October 2019, 19:24:55 UTC |
| baa7046 | jadep | 24 September 2019, 18:55:24 UTC | add Z_mul and change Z_shiftl to Z_truncating_shiftl | 16 October 2019, 19:24:55 UTC |
| ae949fb | jadep | 24 September 2019, 18:18:19 UTC | make of_expr handle Abs | 16 October 2019, 19:24:55 UTC |
| b539114 | jadep | 24 September 2019, 15:17:22 UTC | add Z_add_with_get_carry and replace magic number 2^64 with 2 ^ Semantics.width | 16 October 2019, 19:24:55 UTC |
| 2c9b130 | jadep | 24 September 2019, 14:46:21 UTC | add Z_mul_split | 16 October 2019, 19:24:55 UTC |
| 241772e | jadep | 24 September 2019, 14:34:07 UTC | improve comments | 16 October 2019, 19:24:55 UTC |
| 3d1f10b | jadep | 24 September 2019, 14:19:44 UTC | add land, add, shiftr, and shiftl to of_inner_expr | 16 October 2019, 19:24:55 UTC |
| 0e2f12b | jadep | 23 September 2019, 22:06:52 UTC | tweak the way lists are handled and make of_expr deal with them; introduce extra notations to make debugging nicer | 16 October 2019, 19:24:55 UTC |
| ae7d365 | jadep | 23 September 2019, 19:55:49 UTC | add new test case using list construction and shift | 16 October 2019, 19:24:55 UTC |
| daab1bc | jadep | 23 September 2019, 19:37:07 UTC | add nth_default and literals to of_inner_expr so test_expr4 works | 16 October 2019, 19:24:55 UTC |
| 46b9c5b | jadep | 23 September 2019, 18:49:21 UTC | add new test case with list indices and literals (currently failing); capitalize error to make it more visible in debugging | 16 October 2019, 19:24:55 UTC |
| b9c706a | jadep | 23 September 2019, 18:41:33 UTC | fix up cast logic and add new debug expression | 16 October 2019, 19:24:55 UTC |
