Dan Christensen

I made a mistake in my test, so I take back the previous comment. I can't make Magma behave like pType. Very strange.

It does sound to me like having this set globally is best. I'm not sure what I was thinking when I said that partial typeclass resolution is "correct", because it...

Something short would be great, but I don't mind ``` nrefine (some_lemma _ a _ b); only 1-2,3,5: exact _. ``` or the form with a period that Mike posted...

I tested the default version in Ubuntu (1.21), and it does work. Is this a known issue with the snap? Is there a workaround? I just tested with firefox, which...

Two NVMe drives in software raid 1, /home, lots of small files. ``` workers files dirs bytes time (seconds) bandwidth (per second) 1 100955 11789 11300634506 26.483996109 426696728 2 100955...

Since chunking, compressing, encrypting, etc will take time, will having multiple file traversal threads help much in practice? I guess it will help in the common case where very little...

LGTM modulo the minor issues I pointed out. (Try not to introduce stray unrelated changes.)

Does this mean it won't build with 8.15 anymore? Maybe we should keep compatibility until we have a strong reason to not be compatible, as some users might not have...

Well, even after #1661, the library should still be usable with 8.15. I would prefer to delay removing the compatibility code until we have merged something else that prevents the...

@infectormp Is there a known fix? As far as I know, this hasn't been debugged yet. I've been running with --debug on one machine for a while, and haven't seen...