| 0f249ef | Mario Carneiro | 27 April 2023, 10:44:05 UTC | Improve number07 proof This is starting to see diminishing returns, so I may not continue with these simplifications, but this was the next heavy hitter on the list of compile time records, so I thought I would take a look. There were some very silly proofs that e.g. the divisors of 226 are {1,2,113,226} which proceeded by testing all smaller numbers (where the better proof is to observe that 226 = 2*113 and these are prime). Replacing these with one line proofs resulted in the majority of the size reduction of the file. The second improvement is in the enumeration of all n <= 201 such that "n satisfies_Sierpinski_problem_89". The original proof first proved each case in a separate lemma, then tries to combine them 6 at a time. The problem is that "n satisfies_Sierpinski_problem_89" is defined as a conjunction of three things, so the verifier internally explodes each assumption "not 18 satisfies...", "not 19 satisfies..." etc into 3 cases each, resulting in 6 * 3^6 = 4374 cases being sent to the verifier after expansion and making this proof extremely slow. It turns out that only one in 4 cases actually need to be dealt with explicitly, the rest can be proven impossible without case analysis. Inlining the proofs of "not 18 satisfies..." etc also solves the case explosion problem. The net result: lines: 11310 -> 2267 (80% reduction) verifier: 11:05 -> 0:17 (39x improvement) mizar-rs: 1:24.5 -> 0:02.5 (34x improvement) | 27 April 2023, 10:44:05 UTC |
| 49d66ac | Mario Carneiro | 26 April 2023, 06:00:15 UTC | Minimize xprimes1,2 for massive gains This is the easiest proof optimization I could possibly make and yet it has huge wins on these files. The proof involved a series of steps of the form now 11 = 2*5 + 1; hence not 2 divides 11 by NAT_4:9; 11 = 3*3 + 2; hence not 3 divides 11 by NAT_4:9; 11 = 5*2 + 1; hence not 5 divides 11 by NAT_4:9; 11 = 7*1 + 4; hence not 7 divides 11 by NAT_4:9; end; proving that 11 does not divide any smaller prime, but this is silly since one only needs to check primes up to the square root of 11 (meaning that 5 and 7 in this example are superfluous). Even more surprisingly, *the lemma applied proves exactly this*: in this example we apply a theorem that says "p*p <= k < 25 implies p = 2 or p = 3", so literally all we have to do is delete the steps for 5 and 7 and the proof still goes through. I would have thought that the Mizar tools automatically minimize this sort of thing, but it's possible that the use of "now" is messing things up. In any case, I deleted a bunch of redundant lines, resulting in a 93% reduction in xprimes1 proof lines and a 96% reduction in xprimes2. xprimes1 check time is reduced 20x for verifier and 24.5x for mizar-rs. The memory and disk usage for verifier was also alarmingly high, and I had difficulty running it to completion. I had to kill the verifier run for xprimes2, so the reduction is >28x for verifier and a whopping 69x for mizar-rs. xprimes1: lines: 315577 -> 20730 verifier: 29:33 + 10.8G rss + 6.96G .xml -> 1:25 + 640M rss + 16.3M .xml mizar-rs: 2:08.5 + 30.3M rss -> 0:05.25 + 10.3M rss xprimes2: lines: 453831 -> 15799 verifier: killed at 15:54 + 12.1G rss + 16.9G .xml (out of disk) -> 0:34 + 586M rss + 18.4M .xml mizar-rs: 4:02 + 43.7M rss -> 0:03.5 + 10.7M rss | 26 April 2023, 06:00:15 UTC |
| e1638f9 | Mario Carneiro | 26 April 2023, 02:47:50 UTC | rewrite number04 to be faster This is another major MML modification, which rewrites the core computational part of number04 to use a different proof strategy that is 52% shorter and 19x faster to verify on mizar-rs, 11x faster on `verifier`. In short, rather than calculating `a^n mod b` by working out all the powers of `a` and then modding by `b`, we do the mod during the power calculation, avoiding the need for big numbers. Mizar can handle big numbers just fine, but the large number of numerals and numeral expressions at global scope here pollutes both the term cache and the infer const cache, leading to effectively quadratic performance with the verifier getting slower and slower as it progresses through the file. In the rewrite we put all the numbers inside many little scopes, so there is no buildup of junk. verifier: 3:59 <- 46:16 mizar-rs: 0:17 <- 5:26 + 7 ovfl. err As a result, we are now back to 100% success on the MML. Fixes #3 | 26 April 2023, 02:47:50 UTC |
| 382d959 | Mario Carneiro | 26 April 2023, 02:46:34 UTC | add term cache garbage collection This is a very unsophisticated check, we just clear the cache when it gets above a certain limit. The reasoning is that if the cache becomes too big, then the cost of finding a constant in the cache (which involves O(log N) comparisons to other constants in the cache) grows larger than the cost of reconstructing the term and its type from scratch (the cost of which is proportional to the size of various internal data structures plus the size of the term). The limit used here is somewhat on the high side, and was chosen based on when the cache size starts to visibly slow down verification. | 26 April 2023, 02:46:34 UTC |
| b85f27f | Mario Carneiro | 25 April 2023, 19:15:42 UTC | don't hold whole AST in memory This is a big memory savings for large MML files like xprimes2, by streaming top level items from the parser to the analyzer rather than doing parsing up front and holding the AST until the analyzer is done. | 25 April 2023, 19:15:42 UTC |
| cd4fa10 | Mario Carneiro | 25 April 2023, 18:32:08 UTC | shorten proofs in xprimet1.miz This is our first major modification to the MML. The proofs in article xprimet1 were very inefficient, and it was simpler to fix the proofs rather than to try to make the overflow behavior exactly line up with pascal mizar. The original proofs were clearly automatically generated, and the fixes in this commit are also automatically generated (by an ad-hoc script, not included). | 25 April 2023, 18:32:08 UTC |
| 3589fe5 | Mario Carneiro | 25 April 2023, 08:12:08 UTC | support `$V+` and `$V-` pragmas | 25 April 2023, 08:12:08 UTC |
| 2a4dd30 | Mario Carneiro | 20 April 2023, 19:39:07 UTC | Upgrade to MML v. 8.1.12_5.74.1441 The verifier mostly works on the new MML out of the box, which is good, although they seem to have come up with new and unusual ways to torture the verifier in this edition and some of the new articles have managed to beat the record for longest check time. Some profiling is needed, and possibly some quadratic algorithms need to be revisited. Fixes #1 | 20 April 2023, 19:39:07 UTC |
| 19b80d9 | Mario Carneiro | 20 April 2023, 17:25:34 UTC | Remove dependency on original mizar With a small patch, DEP_ORDER now actually works to read everything from scratch, so we can finally drop the dependency on pascal Mizar entirely, resulting in a whopping 33x improvement in the runtime of analyze-mml.sh. | 20 April 2023, 17:27:20 UTC |
| 9a9618b | Mario Carneiro | 20 April 2023, 14:59:10 UTC | Mizar implementation complete! :tada: This implements the mizar parser infix disambiguation algorithm, and does final testing with all the options enabled. We can now read and verify the entire MML starting only from the .miz files. | 20 April 2023, 14:59:10 UTC |
| 4c944b2 | Mario Carneiro | 17 April 2023, 11:13:32 UTC | Name resolution: debugging (done!) Now tested with analyzer + checker. Enabling by default. | 17 April 2023, 11:44:41 UTC |
| b5fdbbc | Mario Carneiro | 17 April 2023, 09:34:58 UTC | refactoring name resolution | 17 April 2023, 09:40:17 UTC |
| 2ea1c99 | Mario Carneiro | 17 April 2023, 08:32:53 UTC | add source positions to exported theorems | 17 April 2023, 08:32:53 UTC |
| 4462fbb | Mario Carneiro | 17 April 2023, 08:31:26 UTC | Name resolution: more debugging Now tested with VERIFY_EXPORT. | 17 April 2023, 08:31:26 UTC |
| 0545979 | Mario Carneiro | 16 April 2023, 16:00:55 UTC | Name resolution: initial implementation, debugging This is tested on MML in analyzer-quick mode, more modes will wait for the next commit. We have a few more MML patches here. The one in trees_a is due to inconsistency in the Mizar quantifier lifting algorithm; the discrepancies seem to be very rare so I'm okay with that. The extra reservation in msafree5 is because Mizar seems to allow resolving reservations which are dependencies of other reservations to a redeclaration with the same name; this is confusing and rare enough that a patch seems easier than the overhaul and complication of the algorithm. | 16 April 2023, 16:00:55 UTC |
| f6b0a7b | Mario Carneiro | 14 April 2023, 19:14:39 UTC | prepare for nameck pass | 14 April 2023, 19:14:39 UTC |
| c5499c1 | Mario Carneiro | 13 April 2023, 21:50:00 UTC | .miz parser: debugged on MML It can now parse everything without failing, although the results have not yet been tested for correctness (and cannot be until the MSM pass is complete). One slightly unnecessary change which required a patch on MML was the removal of the form `scheme: stmt; end` using a `;` instead of `proof` in `scheme: stmt proof end`. The former syntax makes no sense at all seeing as everywhere else in the language a `;` after a statement means a trivial proof to be done by the checker, and the `end` is confusingly paired. It would not be hard to support, but it's a trivial fix to remove the few cases that were using this variant syntax. | 13 April 2023, 21:50:00 UTC |
| 9d34b05 | Mario Carneiro | 13 April 2023, 10:55:49 UTC | .miz parser: initial implementation | 13 April 2023, 10:55:49 UTC |
| 4569f04 | Mario Carneiro | 03 April 2023, 09:58:40 UTC | add valid aid / nr data to prel The diff to Mizar is now very small; the only thing that remains is the `redefnr` attribute in `write_dno`. | 03 April 2023, 09:58:40 UTC |
| 19869f0 | Mario Carneiro | 03 April 2023, 07:27:40 UTC | improve download flow We have enough implemented that can now use `verifier -p` to run only the parser and use mizar-rs for everything else, including generating the prel/ files. Thus we no longer need a patch file for it. | 03 April 2023, 07:27:40 UTC |
| fd64787 | Mario Carneiro | 03 April 2023, 05:20:39 UTC | cache prel/ files in memory Now we can process the MML without having to look at the prel/ files at all, except for the hand-written ones (hidden, tarski_0, tarski_a and the .dre files). The remaining data files we have to read are {.evl, .frx, .msx, .vcl, .frm} from the mml folder; we will need a mizar parser to eliminate these. | 03 April 2023, 05:20:39 UTC |
| 8013ea3 | Mario Carneiro | 02 April 2023, 06:32:01 UTC | XML export: done | 02 April 2023, 06:32:01 UTC |
| 61a5847 | Mario Carneiro | 01 April 2023, 06:23:38 UTC | XML export: initial implementation | 01 April 2023, 06:23:38 UTC |
| b10fe63 | Mario Carneiro | 31 March 2023, 21:59:30 UTC | cleanup | 31 March 2023, 21:59:30 UTC |
| e7f2b83 | Mario Carneiro | 31 March 2023, 21:39:12 UTC | update README, interface, more timing | 31 March 2023, 21:39:12 UTC |
| dcf66b0 | Mario Carneiro | 31 March 2023, 18:27:30 UTC | accom + analyzer + checker + exporter works on MML! This is a bugfix for a scope check issue in finseq_9 | 31 March 2023, 18:27:30 UTC |
| 3e3dd0b | Mario Carneiro | 31 March 2023, 07:36:52 UTC | Debugging accomodator: done! | 31 March 2023, 07:55:03 UTC |
| 9f19790 | Mario Carneiro | 29 March 2023, 12:06:10 UTC | make unify monotonic Earlier changes have left us with one failure in the MML, so we have to do something about this. This is a simple fix, but it unfortunately comes with a small overhead since we are now considering more potential instantiations. Still, not considering them was pretty much a bug in the first place, leading to strange failures that make no sense from the user perspective. | 29 March 2023, 12:06:10 UTC |
| 5b0591d | Mario Carneiro | 28 March 2023, 04:46:59 UTC | Accomodator: initial implementation | 28 March 2023, 04:46:59 UTC |
| 4ece845 | Mario Carneiro | 23 March 2023, 01:58:22 UTC | update timing chart | 23 March 2023, 01:58:22 UTC |
| 506fe26 | Mario Carneiro | 23 March 2023, 01:52:29 UTC | transfer: cleanup | 23 March 2023, 01:52:29 UTC |
| 4569af2 | Mario Carneiro | 23 March 2023, 01:43:48 UTC | Transfer, part 7: theorems, schemes (done!) | 23 March 2023, 01:43:48 UTC |
| b183b8c | Mario Carneiro | 23 March 2023, 01:15:59 UTC | update Mizar https://github.com/digama0/mizar-system/commit/2dfb42c Unfortunately it seems this bug has a pretty big effect on the prel/ files, which is making this "patch" approach less practical. To make the patch easier to review the MML changes have been split into a separate file; the prel changes are automatically generated by the Mizar patch and are provided for convenience. | 23 March 2023, 01:15:59 UTC |
| f6ba56e | Mario Carneiro | 22 March 2023, 22:27:01 UTC | Transfer, part 6: identities, reductions, properties | 22 March 2023, 22:27:01 UTC |
| e720e40 | Mario Carneiro | 22 March 2023, 22:16:37 UTC | Transfer, part 5: definitions | 22 March 2023, 22:16:37 UTC |
| 4a5df3e | Mario Carneiro | 22 March 2023, 21:21:47 UTC | Transfer, part 4: cluster registrations The big change here is because we need to remove duplicate attributes in the prel/ files for verification because of mizar bugs, but we can't just call `Attr::cmp` because we don't have an appropriate global context. We could create one at some expense, but here we are gambling that none of the really weird cases actually show up and a plain sort without context is sufficient. (So far, it's holding up on the MML.) | 22 March 2023, 21:21:47 UTC |
| bdbf3c3 | Mario Carneiro | 22 March 2023, 20:00:14 UTC | Transfer, part 3: notations | 22 March 2023, 20:00:14 UTC |
| 38665c0 | Mario Carneiro | 22 March 2023, 11:18:17 UTC | upstream the symbol kind bugfix (part 2) https://github.com/digama0/mizar-system/commit/2dfb42c | 22 March 2023, 11:18:17 UTC |
| 18f97d1 | Mario Carneiro | 22 March 2023, 10:00:34 UTC | Transfer, part 2: constructors | 22 March 2023, 10:00:34 UTC |
| b2cb791 | Mario Carneiro | 19 March 2023, 15:27:57 UTC | remove no longer necessary patch | 19 March 2023, 15:27:57 UTC |
| 5409420 | Mario Carneiro | 19 March 2023, 14:45:42 UTC | upstream the symbol kind bugfix https://github.com/digama0/mizar-system/commit/5d83403 | 19 March 2023, 14:45:42 UTC |
| 9ff717f | Mario Carneiro | 19 March 2023, 13:42:38 UTC | Transfer, part 1: formats | 19 March 2023, 13:42:38 UTC |
| 6ab01ea | Mario Carneiro | 19 March 2023, 11:09:48 UTC | add prel patches from fixed mizar Fixed mizar: https://github.com/digama0/mizar-system/commit/3021014 The main upshot of patching mizar and prel/ is that we can eliminate the "expected failure" case. The download-mml.sh script is now slightly incorrect though, as it is still downloading the unpatched mizar. | 19 March 2023, 11:09:48 UTC |
| 54a425e | Mario Carneiro | 18 March 2023, 17:06:17 UTC | debugging exporter: done! | 18 March 2023, 17:06:17 UTC |
| f99096c | Mario Carneiro | 18 March 2023, 16:56:16 UTC | debugging exporter: theorems | 18 March 2023, 16:56:16 UTC |
| f088aea | Mario Carneiro | 18 March 2023, 16:03:01 UTC | debugging exporter: identities, reductions, properties | 18 March 2023, 16:03:01 UTC |
| 9f66e9e | Mario Carneiro | 18 March 2023, 15:29:50 UTC | debugging exporter: definientia | 18 March 2023, 15:29:50 UTC |
| 5815ab1 | Mario Carneiro | 18 March 2023, 15:06:51 UTC | debugging exporter: clusters | 18 March 2023, 15:06:51 UTC |
| 0284d02 | Mario Carneiro | 18 March 2023, 12:56:29 UTC | debugging exporter: constructors | 18 March 2023, 12:56:29 UTC |
| e2a0f74 | Mario Carneiro | 18 March 2023, 07:27:26 UTC | debugging exporter: file 0 | 18 March 2023, 07:27:26 UTC |
| ba27889 | Mario Carneiro | 17 March 2023, 19:00:06 UTC | Exporter, part 1: initial implementation | 17 March 2023, 19:00:06 UTC |
| 3b54098 | Mario Carneiro | 14 March 2023, 07:08:49 UTC | add "analyzer (quick)" mode | 14 March 2023, 07:08:49 UTC |
| 83807fe | Mario Carneiro | 14 March 2023, 03:26:37 UTC | add link to performance comparison | 14 March 2023, 03:26:37 UTC |
| 12ef451 | Mario Carneiro | 14 March 2023, 00:29:25 UTC | update timing chart | 14 March 2023, 00:29:25 UTC |
| 1db847a | Mario Carneiro | 13 March 2023, 13:19:52 UTC | Analyzer is done! (take 2) The previous commit failed to handle failures by panics, including a fair number of analyzer issues. These are now fixed, and we are now the analyzer+checker is tested on the whole MML. | 13 March 2023, 13:19:52 UTC |
| dd1d15a | Mario Carneiro | 10 March 2023, 12:55:49 UTC | Analyzer is done! | 10 March 2023, 12:58:42 UTC |
| 0f6cb28 | Mario Carneiro | 10 March 2023, 08:12:32 UTC | scope-aware eq, runtime config, file 516 | 10 March 2023, 12:04:45 UTC |
| 1e6cd41 | Mario Carneiro | 08 March 2023, 06:43:30 UTC | debugging analyzer: file 512 | 08 March 2023, 06:43:30 UTC |
| 527d072 | Mario Carneiro | 05 March 2023, 10:53:42 UTC | debugging analyzer: file 279 This one is really painful, because of a combination of two things: * Resolution of implicit arguments is dependent on attribute order. For example, given: definition let A be set, B be A-valued Relation; func foo B -> set means ...; end; If we have `A being X-valued Y-valued Relation` then `foo A` could mean either `foo[X] A` or `foo[Y] A`. It is important which one is chosen as the checker can prove different facts about them. In Mizar, it resolves to the first attribute in the list. * Mizar has some bugs which cause it to not actually sort attributes correctly, so we can't just keep the attributes sorted, we have to follow the same buggy algorithm as Mizar if we want to check MML. | 05 March 2023, 10:53:42 UTC |
| 09751f8 | Mario Carneiro | 04 March 2023, 10:02:43 UTC | debugging analyzer: file 168 | 04 March 2023, 10:02:43 UTC |
| 52a43f3 | Mario Carneiro | 04 March 2023, 07:43:30 UTC | debugging analyzer: file 72 | 04 March 2023, 07:43:30 UTC |
| 7a39720 | Mario Carneiro | 04 March 2023, 02:45:40 UTC | debugging analyzer: file 30 | 04 March 2023, 02:45:40 UTC |
| 69840ff | Mario Carneiro | 04 March 2023, 00:18:35 UTC | debugging analyzer: file 22 | 04 March 2023, 00:18:35 UTC |
| 40eb063 | Mario Carneiro | 03 March 2023, 06:35:53 UTC | debugging analyzer: file 18 | 03 March 2023, 06:37:08 UTC |
| d55cf7b | Mario Carneiro | 03 March 2023, 05:02:37 UTC | debugging analyzer: file 11 | 03 March 2023, 05:02:37 UTC |
| db46b0c | Mario Carneiro | 01 March 2023, 22:55:15 UTC | debugging analyzer: file 9 | 01 March 2023, 23:43:45 UTC |
| c320e05 | Mario Carneiro | 23 February 2023, 08:31:13 UTC | more readme | 23 February 2023, 08:31:13 UTC |
| b1eb24b | Mario Carneiro | 23 February 2023, 08:16:25 UTC | reproducible build, add README | 23 February 2023, 08:16:25 UTC |
| 059491c | Mario Carneiro | 22 February 2023, 10:35:10 UTC | Add GPLv3 license This is a derivative of the GPL licensed Mizar project (https://github.com/MizarProject/system), hence it is also GPL licensed. | 22 February 2023, 10:35:10 UTC |
| 8eb4aa6 | Mario Carneiro | 22 February 2023, 10:28:45 UTC | tweaks | 22 February 2023, 10:28:45 UTC |
| 9b7f73b | Mario Carneiro | 19 February 2023, 07:30:24 UTC | debugging analyzer: file 8 | 19 February 2023, 07:30:24 UTC |
| 7f48d65 | Mario Carneiro | 18 February 2023, 06:07:22 UTC | debugging analyzer: file 2 | 18 February 2023, 06:07:22 UTC |
| eec3b74 | Mario Carneiro | 17 February 2023, 23:33:35 UTC | debugging analyzer: file 0 | 17 February 2023, 23:33:35 UTC |
| dd06465 | Mario Carneiro | 16 February 2023, 21:33:09 UTC | re-bugfix the checker since we added a bunch of stuff and in particular changed FlexAnd handling. Unfortunately it's not all roses, we now have a real unsoundness in the checker which cannot be fixed without breaking MML. | 16 February 2023, 21:33:34 UTC |
| e7d0d3f | Mario Carneiro | 15 February 2023, 11:09:34 UTC | Analyzer part 13: flex-and elaboration (and we're done!) | 15 February 2023, 11:09:34 UTC |
| 4655c8b | Mario Carneiro | 15 February 2023, 08:05:31 UTC | change FlexAnd representation I was planning to do this eventually anyway, but it turns out that the existing representation actually has a soundness bug, in addition to the sketchy unpacking code in `expand()`, because it is not true that equality of the endpoints implies equality of the FlexAnd expressions. For example, `P[1+1] /\ ... /\ P[n]` represents `P[x]` for `x in 1..=n` but if you substitute `n = 2+2` then you get the expression `P[1+1] /\ ... /\ P[2+2]`, which if re-parsed actually results in `P[x+x]` for `x in 1..=2`. These two expressions are not equivalent despite having the same endpoints and this can be used to prove false. | 15 February 2023, 08:08:39 UTC |
| f498ae7 | Mario Carneiro | 15 February 2023, 04:43:37 UTC | Analyzer part 12: properties | 15 February 2023, 04:43:37 UTC |
| 106d58b | Mario Carneiro | 12 February 2023, 07:51:33 UTC | Analyzer part 11: notations (synonym/antonym) | 12 February 2023, 07:51:33 UTC |
| 6fd75cc | Mario Carneiro | 11 February 2023, 16:10:03 UTC | Analyzer part 10.6: sethood registrations | 11 February 2023, 16:10:03 UTC |
| aca18d1 | Mario Carneiro | 11 February 2023, 15:46:53 UTC | Analyzer part 10.5: reduction registrations | 11 February 2023, 15:46:53 UTC |
| 4bf7dd4 | Mario Carneiro | 11 February 2023, 14:20:30 UTC | Analyzer part 10.4: identify registrations | 11 February 2023, 14:20:30 UTC |
| 1260a3d | Mario Carneiro | 06 February 2023, 11:06:09 UTC | Analyzer part 10.3: conditional registrations | 06 February 2023, 11:06:09 UTC |
| 8ffcb29 | Mario Carneiro | 06 February 2023, 10:30:49 UTC | Analyzer part 10.2: functor registration | 06 February 2023, 10:30:49 UTC |
| 5e328be | Mario Carneiro | 06 February 2023, 08:43:53 UTC | Analyzer part 10.1: existential cluster registration | 06 February 2023, 08:43:53 UTC |
| 20a541f | Mario Carneiro | 06 February 2023, 05:55:57 UTC | Analyzer part 9: structure definitions | 06 February 2023, 05:55:57 UTC |
| 37f81fc | Mario Carneiro | 30 January 2023, 05:20:13 UTC | extract functions | 30 January 2023, 05:20:13 UTC |
| cf046b8 | Mario Carneiro | 30 January 2023, 05:11:28 UTC | Analyzer part 8.6: functor definitions | 30 January 2023, 05:11:28 UTC |
| 0d08008 | Mario Carneiro | 30 January 2023, 03:32:50 UTC | Analyzer part 8.5: attribute definitions | 30 January 2023, 03:32:50 UTC |
| 062b034 | Mario Carneiro | 30 January 2023, 01:57:27 UTC | Analyzer part 8.4: predicate definitions | 30 January 2023, 01:57:27 UTC |
| 855dad0 | Mario Carneiro | 29 January 2023, 23:43:37 UTC | Analyzer part 8.3: expandable mode definitions | 29 January 2023, 23:43:37 UTC |
| f6be949 | Mario Carneiro | 29 January 2023, 23:13:59 UTC | Analyzer part 8.2: mode redefinitions | 29 January 2023, 23:13:59 UTC |
| d6a47f2 | Mario Carneiro | 29 January 2023, 14:48:25 UTC | Analyzer part 8.1: mode definitions | 29 January 2023, 14:48:25 UTC |
| 4103d8d | Mario Carneiro | 24 January 2023, 22:15:36 UTC | Analyzer part 7: non-proof block structure | 24 January 2023, 22:15:36 UTC |
| e6d8e30 | Mario Carneiro | 18 January 2023, 23:48:40 UTC | Analyzer part 6: inferences | 19 January 2023, 00:25:22 UTC |
| 886d060 | Mario Carneiro | 18 January 2023, 23:31:55 UTC | Analyzer part 5: private statements | 19 January 2023, 00:24:53 UTC |
| f81a3d0 | Mario Carneiro | 18 January 2023, 21:37:32 UTC | Analyzer part 4: WHNF, proof skeleton steps | 18 January 2023, 21:37:32 UTC |
| 8d5a91f | Mario Carneiro | 18 January 2023, 12:33:24 UTC | Analyzer part 3: thesis reconstruction | 18 January 2023, 12:33:24 UTC |
| deda160 | Mario Carneiro | 17 January 2023, 00:52:43 UTC | Analyzer part 2: proof skeleton steps | 17 January 2023, 00:53:52 UTC |
| 58ca6c1 | Mario Carneiro | 13 January 2023, 13:33:13 UTC | Analyzer part 1: elaborating terms/types/formulas | 13 January 2023, 13:33:13 UTC |
| 75154b3 | Mario Carneiro | 13 January 2023, 13:26:54 UTC | allow borrowed expressions in Subst | 13 January 2023, 13:27:47 UTC |
