Ramana Kumar
Ramana Kumar
#### System information Geth version: `geth version` ``` Geth Version: 1.10.4-stable Git Commit: aa637fd38a379db6da98df0d520fb1c5139a18ce Git Commit Date: 20210617 Architecture: amd64 Go Version: go1.16.5 Operating System: linux GOPATH= GOROOT=go ``` OS...
`EVERY2` and `LIST_REL` are the same constant (one is an overload for the other). But several theorems use "EVERY2" in their name, which makes it hard to find theorems about...
The various tacticals (`THEN`, `THENL`, `THEN1`) could be made to parallelise evaluation of the tactics on multiple subgoals. (I think it's reasonable to treat tactics that aren't robust to such...
There are two `Holmakefile` functions that, from a user's perspective, serve the same purpose: namely, protect strings that contain spaces or other unusual characters from being split into multiple items...
I propose a mode for `Holmake` to detect and warn about redundant `INCLUDES`, i.e., directories that are included but for which no dependencies are found for any targets in the...
Similar to #488 but less extreme: Could we have a cache of theorems that have been proved before so that when this option is turned on any attempts to prove...
The proof manager could keep a cache of previously seen and proved subgoals, and prove them immediately if they are seen again. This might speed up interactive development with long-running...
This would for example avoid cascading rebuilds if you just add a comment to a script file (and it produces exactly the same theory).
I notice that if one has `CLINE_OPTIONS` in the `Holmakefile` set to `-j1`, then this is propagated to recursive `Holmake` calls in `INCLUDES` directories as well. I guess this fits...
One would hope `ListConv1.ALL_EL_CONV` to be an efficient specialised conversion for evaluating `EVERY _ _` terms, but it actually performs much worse than `EVAL`. If it can't be made to...