Daniel Selsam

> One easy (but weird) fix is to disallow sizeof in compiled code. That is, sizeof is used only for justifying well-founded recursion. [Wearing my (on-and-off) developer hat] I like...

> may become increasingly problematic I thought I would mention that this is no longer a hypothetical concern for me. Even though I don't use any automation besides occasionally calling...

I wrote a proposal a few months back for organizing the trace messages which is germane to this discussion: https://github.com/leanprover/lean4/issues/400#issuecomment-819752356 I still think this proposal is basically right and that...

Yes, this could be a big win. I hope the trace explorer will let us be less conservative in collecting trace messages in the first place. Thanks to filtering and...

`simp` recurses a linear number of times on these examples, and the time within the `simp` tactic seems linear even out to 4000: ``` [4000] 1628ms 46.2% tactic.simplify [2000] 830ms...

- I thought https://github.com/leanprover-community/mathport/commit/61b4659b7bcbf2c61b09db8370487b6f78403701 would solve the `hom` issue -- I even had a self-contained file that I thought mimic-ed the setup that the commit fixed. - `class category_struct` and...

It looks like the parser doesn't actually resolve the `hom` at all, because the parser does not know it is in the namespace of the extends when it parses the...

I tracked down my original schema file and made a gist: https://gist.github.com/dselsam/cd0f46c3ca366120c6074bf73d49a1f9

Note: the problems take up a ton of space.

No. If I recall, many of the SATCOMP downloads were unreliable back then and I ended up retrying a lot manually at different times.