Jason Gross
Jason Gross
Why does the Lean Importer require an unsafe hierarchy?
Am I missing something? Is the thunking in `Control.refine` used for more than management of the shelved status of goals, i.e., is `Control.refine (fun () => f ())` not identical...
Okay, on my concrete issue, `Control.refine (fun () => f ())` results in (improper) instantiation of additional evars, relative to `Control.unshelve (fun () => let c := f () in...
Note that Arch is on 9.1 as per https://repology.org/project/rocq/versions but does not package stdlib, so the stdlib split has resulted in Fiat Crypto's CI failing on Arch
And it seems like this message is incorrect, even? Unless EACCES is an extremely poor error message for "file does not exist". When I `ls -la /__w/_temp/_runner_file_commands`, [I get](https://github.com/mit-plv/fiat-crypto/actions/runs/7321168614/job/19941201055?pr=1798#step:7:24) ```...
I am becoming more convinced that this may be a bug with the checkout action. Is it fundamentally incompatible with containers where the current user/group ids do not match those...
Possibly a duplicate of https://github.com/actions/checkout/issues/956 ?
It seems that `Notation "'foo'" := bar (in custom baz at level n).` already only introduces a keyword for n > 0
> I guess mostly it feels rather non modular (what happens if separate modules register the same character?) Oh, I guess the issue is that format settings are interpreted at...