Ali Caglayan (May 09 2022 at 10:00): Ali Caglayan (May 09 2022 at 10:00):What is stopping us from doing https://github.com/coq/coq/issues/13394 in 8.16?
Gaëtan Gilbert (May 09 2022 at 10:02):laziness
Ali Caglayan (May 09 2022 at 10:03):If we turn the warning into an error, will it just become an overlay writing exercise?
Pierre-Marie Pédrot (May 09 2022 at 10:13):yes, conceptually trivial but annoying in practice
Pierre-Marie Pédrot (May 09 2022 at 10:14):if you're brave enough to do it before the branch I'd support such an endeavour
Pierre-Marie Pédrot (May 09 2022 at 10:14):(expect quite a bit of work between writing overlays and getting them merged)
Ali Caglayan (May 09 2022 at 10:35):We do however want to eventually introduce a default hint locality in the future right?
Ali Caglayan (May 09 2022 at 10:35):So I won't get rid of default_hint_locality but instead throw an error on its use?
Gaëtan Gilbert (May 09 2022 at 10:35):make the warning AsError
Ali Caglayan (May 09 2022 at 10:43):Let's see what happens: https://github.com/coq/coq/pull/16004
Ali Caglayan (May 09 2022 at 11:47):Alright test-suite is the first causality, I'll work on that first.
Ali Caglayan (May 09 2022 at 12:23):There is also a warning for Hint Rewrite should I make that an error too?
Gaëtan Gilbert (May 09 2022 at 12:25):check what version it was made, if it's had a version as a warning then yes
Ali Caglayan (May 09 2022 at 12:34):That was 8.14 it seems
Ali Caglayan (May 09 2022 at 12:35):I will do their cleanup separately however just in case
Pierre-Marie Pédrot (May 09 2022 at 12:41):The hard part is writing the overlays, fixing the bug on the Coq side is just a one-liner.
Pierre-Marie Pédrot (May 09 2022 at 13:35):@Ali Caglayan do you need help to write the overlays?
Ali Caglayan (May 09 2022 at 13:36):I would welcome help on that
Pierre-Marie Pédrot (May 09 2022 at 13:36):(I think that if we want this to happen for 8.16 we'd need a bit more manpower.)
Ali Caglayan (May 09 2022 at 13:36):I'm still messing around with the test-suite
Ali Caglayan (May 09 2022 at 13:36):I'm trying to come up with a killer regexp
Pierre-Marie Pédrot (May 09 2022 at 13:37):there is the script that helps you tracking this
Ali Caglayan (May 09 2022 at 13:37):So far I had
^(?<!Global)(?<!Local )(?<!#[local] )(?<!#[global] )Hint(?! Rewrite)
but this doesn't catch everything
Pierre-Marie Pédrot (May 09 2022 at 13:37):but then the problem is more the interaction with the build system
Gaëtan Gilbert (May 09 2022 at 13:38):add -w -the-warning-name to get_coq_prog_args in the makefile
the test suite shouldn't care about this warning
Gaëtan Gilbert (May 09 2022 at 13:38):(and add it to the _coqproject so editing works right)
Pierre-Marie Pédrot (May 09 2022 at 13:41):@Gaëtan Gilbert do you have a bit of spare time to write some overlays ?
Pierre-Marie Pédrot (May 09 2022 at 13:46):I count 4 such warnings, they're all part of 8.15 right?
Pierre-Marie Pédrot (May 09 2022 at 13:46):-arg "-w +deprecated-hint-rewrite-without-locality"
-arg "-w +deprecated-hint-without-locality"
-arg "-w +deprecated-typeclasses-transparency-without-locality"
-arg "-w +deprecated-instance-without-locality"
The first is from 8.14
Ali Caglayan (May 09 2022 at 14:03):I don't know about the last 2
Ali Caglayan (May 09 2022 at 14:03):I think it is better to do one at a time for now
Ali Caglayan (May 09 2022 at 14:04):I don't believe hint rewrite is nearly as common
Ali Caglayan (May 09 2022 at 14:07):Doing the overlay for argosy rn
Pierre-Marie Pédrot (May 09 2022 at 14:17):on bignums
Ali Caglayan (May 09 2022 at 14:17):argosy is vendoring coq-classes as a submodule so I submitted a patch there, hopefully we can bump that submodule later https://github.com/tchajed/coq-classes/pull/1
Pierre-Marie Pédrot (May 09 2022 at 14:19):the overlays should be performed for all these warnings at once otherwise we'll lose time for the next change
Pierre-Marie Pédrot (May 09 2022 at 14:19):(they will be all backwards compat)
Ali Caglayan (May 09 2022 at 14:22):Shall I make them all errors then?
Pierre-Marie Pédrot (May 09 2022 at 14:24):we'll see for your PR, I think that now the important parts are the overlays
Pierre-Marie Pédrot (May 09 2022 at 14:27):on geocoq
Ali Caglayan (May 09 2022 at 14:30):on mtac2
Ali Caglayan (May 09 2022 at 14:38):deprecated-typeclasses-transparency-without-locality is 8.15
Pierre-Marie Pédrot (May 09 2022 at 14:38):ok
Ali Caglayan (May 09 2022 at 14:38):deprecated-instance-without-locality is 8.14 so I will add that too
Pierre-Marie Pédrot (May 09 2022 at 14:38):(we don't have a ci on https://github.com/coq-community/bignums/pull/70? This looks a bit fragile given that it's a critical piece of software in the dependency graph of coq)
Ali Caglayan (May 09 2022 at 14:39):Only on push to master it seems https://github.com/coq-community/bignums/blob/059f1738ea3409f3d3dbf805d144878de3170fc7/.github/workflows/docker-action.yml#L11
Ali Caglayan (May 09 2022 at 14:41):@Karl Palmskog Do you remember why this is?
Gaëtan Gilbert (May 09 2022 at 14:42):the closed PRs have CI
Karl Palmskog (May 09 2022 at 14:42):there is no problem with the CI configuration. It's GitHub that disables CI workflows after some number of days of inactivity
Karl Palmskog (May 09 2022 at 14:42):please do a force-push and you should get CI now
Ali Caglayan (May 09 2022 at 14:44):Huh weird
Pierre-Marie Pédrot (May 09 2022 at 14:44):seems to have worked (cc @Pierre Roux btw)
Ali Caglayan (May 09 2022 at 14:52):I'm getting dynlink errors doing the overlay for mtac2 so giving up
Karl Palmskog (May 09 2022 at 14:53):for the record @Pierre-Marie Pédrot @Gaëtan Gilbert if you notice something like this again (missing CI for a coq-community project), you can go to the "Actions" tab, and there should be a warning there for "Docker CI". If you click on the warning, there is a button to re-enable CI
Théo Zimmermann (May 09 2022 at 14:54):IINM, this is related to a repository having scheduled workflows.
Ali Caglayan (May 09 2022 at 14:55):on deriving
Théo Zimmermann (May 09 2022 at 14:55):We should remove the scheduled workflow from bignums IMHO.
Théo Zimmermann (May 09 2022 at 14:56):Ali Caglayan said:
deprecated-typeclasses-transparency-without-locality is 8.15
I don't think that make it a problem for making it a fatal warning in 8.16.
Ali Caglayan (May 09 2022 at 20:52):on category_theory
Ali Caglayan (May 09 2022 at 21:30):on color
Ali Caglayan (May 09 2022 at 21:30):on menhir
Ali Caglayan (May 09 2022 at 22:06):Can somebody add me to the INRIA gitlab?
Pierre-Marie Pédrot (May 10 2022 at 06:25):@Ali Caglayan you need an account there, right? I can invite you if this is the case.
Ali Caglayan (May 10 2022 at 07:48):@Pierre-Marie Pédrot Yes, I need one.
Pierre-Marie Pédrot (May 10 2022 at 08:12):Please send me you preferred email address for the account in a private message then.
Pierre-Marie Pédrot (May 10 2022 at 08:14):(I seize the opportunity to complain about the use of the closed INRIA gitlab for CI devs.)
Ali Caglayan (May 10 2022 at 08:21):I am struggling to port math_classes since my crude find-and-replace seems to have changed the meaning of =??
Ali Caglayan (May 10 2022 at 08:22):I would appreciate if somebody could take a look at it with me.
Gaëtan Gilbert (May 10 2022 at 08:25):link?
Ali Caglayan (May 10 2022 at 08:33):I'll push in a sec
Ali Caglayan (May 10 2022 at 08:34):For some reason github got stuck forking
Pierre-Marie Pédrot (May 10 2022 at 08:35):@Ali Caglayan you're not using the "official" porting script based on warning output?
Ali Caglayan (May 10 2022 at 08:35):@Gaëtan Gilbert https://github.com/Alizter/math-classes/tree/adapt-to-16004
Ali Caglayan (May 10 2022 at 08:36):Pierre-Marie Pédrot said:
Ali Caglayan you're not using the "official" porting script based on warning output?
No I though that was just a find and replace so I have been doing find and replace. :O
Pierre-Marie Pédrot (May 10 2022 at 08:36):ah, but then the problem with find and replace is that you may screw up the section hints
Paolo Giarrusso (May 10 2022 at 08:37):That makes local instances global, indeed
Paolo Giarrusso (May 10 2022 at 08:37):(That = I looked at the diff)
Pierre-Marie Pédrot (May 10 2022 at 08:37):Hopefully the overlays you already wrote are not behaviour-changing...
Ali Caglayan (May 10 2022 at 08:38):Hmm it should only be Hint (not Rewrite) inside a section with no locality that gets affected
Ali Caglayan (May 10 2022 at 08:39):oh dear maybe I was too zealous
Pierre-Marie Pédrot (May 10 2022 at 08:39):Hint inside a section can't be global IIRC, but instances can.
Ali Caglayan (May 10 2022 at 08:39):Ah ok then its not so bad probably
Ali Caglayan (May 10 2022 at 08:39):I didn't change Instances too eagerly
Pierre-Marie Pédrot (May 10 2022 at 08:39):well, it means that TC-heavy devs are probably broken
Ali Caglayan (May 10 2022 at 08:40):I'll go and mark them as potentially broken then
Pierre-Marie Pédrot (May 10 2022 at 08:40):(I double-checked and indeed this only affects instances.)
Ali Caglayan (May 10 2022 at 08:40):This probably explains why math-classes didn't work
Pierre-Marie Pédrot (May 10 2022 at 08:41):(Hint Rewrite is also immune to the problem because it doesn't allow global in a section either)
Pierre-Marie Pédrot (May 10 2022 at 08:42):I can write the mathclasses patch if you want
Ali Caglayan (May 10 2022 at 08:42):Sure
Ali Caglayan (May 10 2022 at 08:42):I also couldn't finish verdi_raft
Ali Caglayan (May 10 2022 at 08:42):Probably for the same reason
Ali Caglayan (May 10 2022 at 08:42):Though all its deps are fine
Ali Caglayan (May 10 2022 at 08:43):verdi_raft just hangs for me, after a few changes
Pierre-Marie Pédrot (May 10 2022 at 08:43):TC search maybe?
Ali Caglayan (May 10 2022 at 08:45):probably, I can't workout how to drop into coqide so I can't see it for myself
Pierre-Marie Pédrot (May 10 2022 at 08:47):I do spot suspicious global flags for section instances in e.g. https://github.com/uwplse/verdi/pull/132/files
Pierre-Marie Pédrot (May 10 2022 at 08:49):https://github.com/coq-community/math-classes/pull/111
Ali Caglayan (May 10 2022 at 08:49):Pierre-Marie Pédrot said:
Why did you disable the warnings?
Pierre-Marie Pédrot (May 10 2022 at 08:50):it's actually activating it, but it was a missing git amend from myself, I've forced-pushed
Ali Caglayan (May 10 2022 at 08:51):Now that I think about it category_theory is also probably messed up
Ali Caglayan (May 10 2022 at 08:51):I didn't really question the huge amount of time it took to compile before
Ali Caglayan (May 10 2022 at 08:51):But now I think it might be tc going haywire
Pierre-Marie Pédrot (May 10 2022 at 08:51):meh
Pierre-Marie Pédrot (May 10 2022 at 08:51):in that case you should probably close your PRs that mention instances
Pierre-Marie Pédrot (May 10 2022 at 08:52):FTR here's the script I used to port stuff: https://gist.github.com/ppedrot/3e0c7cbabd9042474c13c25dafefa677
Pierre-Marie Pédrot (May 10 2022 at 08:53):you just set the warnings in the build system, redirect the stderr output to some file log and call the script on that file
Pierre-Marie Pédrot (May 10 2022 at 08:56):dafuq? math_classes has a CI that goes back to Coq 8.6
Ali Caglayan (May 10 2022 at 08:59):https://github.com/uwplse/cheerios/pull/10 looks fine right? I don't think any of those are in sections, just modules.
Ali Caglayan (May 10 2022 at 09:00):Ok I've closed most of the ones I suspect to be broken
Ali Caglayan (May 10 2022 at 09:03):I can't fork menhir because "I've reached my project limit"
Pierre-Marie Pédrot (May 10 2022 at 09:03):interesting...
Ali Caglayan (May 10 2022 at 09:04):I also think I may have botched it anyway so I probably won't bother
Pierre-Marie Pédrot (May 10 2022 at 09:04):I can port it then
Ali Caglayan (May 10 2022 at 09:05):I'll work on perf test
Ali Caglayan (May 10 2022 at 09:11):@Pierre-Marie Pédrot Shall I add that script to tools/ so that other users can use it?
Pierre-Marie Pédrot (May 10 2022 at 09:13):I don't think so, it has been advertised already and it's pretty specific
Pierre-Marie Pédrot (May 10 2022 at 09:14):How does menhirlib work w.r.t. versioning? We're picking a specific tag that is one year old, but there has been activity since.
Pierre-Marie Pédrot (May 10 2022 at 09:15):In particular all the global warnings were fixed in master already
Ali Caglayan (May 10 2022 at 09:36):I guess menhir is good to have in the CI since it uses a lot of coq features. Why we are not tracking the master I don't know. I guess we can fast forward to a more recent commit.
Pierre-Marie Pédrot (May 10 2022 at 09:51):I've written a PR for color: https://github.com/fblanqui/color/pull/42
Ali Caglayan (May 10 2022 at 10:48):perf tests seems to output warnings in stdout :/
Ali Caglayan (May 10 2022 at 10:48):Will the script work when other stuff is in there?
Ali Caglayan (May 10 2022 at 11:22):It doesn't really work for makefiles that call other makefiles
Ali Caglayan (May 10 2022 at 11:22):I give up on perf tests then
Ali Caglayan (May 10 2022 at 11:23):I managed to do VST that was easy, all of the work was already done
Ali Caglayan (May 10 2022 at 11:23):I don't know how to pass flags in Unimath
Ali Caglayan (May 10 2022 at 11:24):I haven't touched any of the fiat stuff except for rewriter
Ali Caglayan (May 10 2022 at 11:25):AFAICT they want to keep their backwards compatibility as much as possible, so I guess we will disable warnings instead
Ali Caglayan (May 10 2022 at 11:37):see https://github.com/mit-plv/rewriter/pull/42
Pierre-Marie Pédrot (May 10 2022 at 11:38):I think that disabling warnings is just putting the dust under the rug.
Pierre-Marie Pédrot (May 10 2022 at 11:38):It will bite us when we want to switch anyways.
Ali Caglayan (May 10 2022 at 11:41):I'm working on category_theory again trying to do it properly this time
Théo Zimmermann (May 10 2022 at 11:44):Pierre-Marie Pédrot said:
I don't think so, it has been advertised already and it's pretty specific
IMHO it should be advertised again if we make these warnings fatal in 8.16. Especially now that it has been battle-tested.
Théo Zimmermann (May 10 2022 at 11:44):Ali Caglayan said:
I guess menhir is good to have in the CI since it uses a lot of coq features. Why we are not tracking the master I don't know. I guess we can fast forward to a more recent commit.
This probably is because it used to be a non-Coq dependency for menhirlib. But now I think the two are in the same repo.
Théo Zimmermann (May 10 2022 at 11:45):Pierre-Marie Pédrot said:
It will bite us when we want to switch anyways.
Especially true if we switch right after branching.
Pierre-Marie Pédrot (May 10 2022 at 11:49):I'm not super fond of doing this change in 8.16 given the current state of affairs.
Pierre-Marie Pédrot (May 10 2022 at 11:50):I'd rather try to fix the CI as much as possible so that the amount of work is limited when we really perform the warning > error switch.
Ali Caglayan (May 10 2022 at 11:53):I guess there is no rush to do it now, but at some point it had to be done.
Ali Caglayan (May 10 2022 at 12:06):Pierre-Marie Pédrot said:
I'm not super fond of doing this change in 8.16 given the current state of affairs.
What exactly do you mean by current state of affairs?
Ali Caglayan (May 10 2022 at 12:06):If it is about the CI then surely we can fix it?
Pierre-Marie Pédrot (May 10 2022 at 12:08):The fact that there are some devs that make strong commitment on supporting pretty old Coq versions. This is reasonable (to some extent).
Pierre-Marie Pédrot (May 10 2022 at 12:09):While striving to support 8.6 is probably not reasonable, 8.13 or so is not utterly crazy.
Pierre-Marie Pédrot (May 10 2022 at 12:10):Also there are some devs which are probably nasty like fcl.
Ali Caglayan (May 10 2022 at 12:15):fcl?
Ali Caglayan (May 10 2022 at 12:15):Did you mean tcl?
Pierre-Marie Pédrot (May 10 2022 at 12:15):fiat-crypto-legacy
Ali Caglayan (May 10 2022 at 12:16):OK so you want to give them more time to have a longer string of compatible versions?
Pierre-Marie Pédrot (May 10 2022 at 12:17):Let's see what they say first, but I don't mind postponing the change to one more version.
Ali Caglayan (May 10 2022 at 12:19):How bad do you think bedrock2 will be?
Ali Caglayan (May 10 2022 at 12:20):I might start it...
Ali Caglayan (May 10 2022 at 12:33):It's looking messy :(
Pierre-Marie Pédrot (May 11 2022 at 09:53):FWIW I'm on unimath
Pierre-Marie Pédrot (May 11 2022 at 10:02):it was surprisingly easy, they basically declare no hints except in their prelude
Ali Caglayan (May 11 2022 at 15:19):category theory done
Ali Caglayan (May 11 2022 at 15:21):@Jason Gross You say for rewriter that you would rather have your hint localities silently export and fix it when this happens, what is wrong with dropping support for older versions and fixing it properly now?
Jason Gross (May 11 2022 at 15:22):@Ali Caglayan I don't plan to drop support for older versions when the default behavior changes, I plan to fix it in a way that is backwards compatible.
Ali Caglayan (May 11 2022 at 15:24):Will you wait until we switch the locality and everything breaks to fix it or fix it before?
Ali Caglayan (May 11 2022 at 15:24):In that case, your fixes will be doing the job of our overlays.
Ali Caglayan (May 11 2022 at 15:25):It looks like this won't make it to 8.16 anyway, so there is around 6 months to fix everything give or take
Ali Caglayan (May 11 2022 at 15:25):Is this the same for fiat_crypto etc. too?
Jason Gross (May 11 2022 at 15:27):I'm inclined to wait until there is at least an option to change the default locality, so that there's no chance of regression (because the option will be a no-op on older versions of Coq and CI will test newer versions of Coq). (Speaking of which, how do you / the devs feel about adding a deprecated option to change default locality?) Once this option exists, I can make the change (for rewriter, bbv, f-c-l, fiat-crypto, and to some extent coqutil; for bedrock2 and rupicola we drop version support much more quickly).
Gaëtan Gilbert (May 11 2022 at 15:31):there's no option plan is there?
Pierre-Marie Pédrot (May 11 2022 at 15:32):The option plan is literally already there.
Ali Caglayan (May 11 2022 at 17:14):@Pierre-Marie Pédrot You mean that there is currently an option to do this in Coq? What is it called, I cannot find it.
Paolo Giarrusso (May 11 2022 at 19:36):@Jason Gross when you say “the option will be a no-op on older versions of Coq”, you must mean “we will not pass the option to older Coq versions” I suppose (say, you’ll autogenerate _CoqProject through conditional compilation)? Otherwise I’m not sure adding the option is technically possible.
Paolo Giarrusso (May 11 2022 at 19:42):Whether devs are willing to provide it is another matter. Could you enlighten us why you still support Coq 8.6? Is that because the cryptography code from fiat-crypto has active non-Coq users on older distributions?
Paolo Giarrusso (May 11 2022 at 19:44):In that case, I wonder if the code generation should be done upstream and the pre-generated C should be distributed for older distros, but there might be complexities there too.
Ali Caglayan (May 11 2022 at 20:28):Paolo Giarrusso said:
Jason Gross when you say “the option will be a no-op on older versions of Coq”, you must mean “we will not pass the option to older Coq versions” I suppose (say, you’ll autogenerate
_CoqProjectthrough conditional compilation)? Otherwise I’m not sure adding the option is technically possible.
If I do
Set Option "foo".
it just throws a warning.
Jason Gross (May 11 2022 at 22:22):Let me lay out my plan all in one place:
Fiat Crypto supports the latest Ubuntu LTS and Debian Stable. I think these versions don't support Global Hint Rewrite, but if they do I'm happy to explicitly annotate. (I would like to eventually switch to #[export], once the Ubuntu LTS / Debian Stable versions of Coq support it.). Part of the sales pitch of fiat-crypto is that users can generate code for new primes, so I'd prefer to maintain out-of-the-box compatibly with these distributions.
Fiat Crypto Legacy supports back to 8.7. There is no pressing reason to keep this support in place, as indeed there are no users of f-c-l other than Coq's CI and anyone that is trying to do archeology on the code from our 2019 paper. However, I'd like to keep this support in place as long as it doesn't incur too much burden.
My plan, for Fiat Crypto Legacy, bbv, and for Fiat Crypto and the rewriter if necessary, is:
Exports module that re-exports the Exports modules of all files that it requires, and stick the necessary hints in these modules. However, as I'd like to eventually move to #[export] behavior, I will aim to be less sledgehammery about following the export discipline. Since no file will rely on default-export hints not being available via Require, and all files will work with default-export behavior, this should be backwards compatible.Set Foo is a no-op for unrecognized Foo) to enforce that the CI checks compatibility with the upcoming default behavior Paolo Giarrusso (May 12 2022 at 06:37):https://packages.ubuntu.com/jammy/coq is 8.15.0, but https://packages.debian.org/bullseye/coq uses 8.12.0 and https://wiki.debian.org/DebianReleases implies the next release is expected around (late) next year, so after Coq 8.18.
Paolo Giarrusso (May 12 2022 at 06:48):I now suspect the option might be Set Loose Hint Behavior "Strict", which was available in 8.12! But it seems to affect only Hint Resolve and Instance: https://coq.inria.fr/distrib/V8.12.2/refman/proof-engine/tactics.html#coq:opt.loose-hint-behavior.
Paolo Giarrusso (May 12 2022 at 06:53):but as defined, that seems to affect even hints that are explicitly marked #[global], instead of just unannotated hints?
Théo Zimmermann (May 12 2022 at 08:10):FTR @Jason Gross, your strategy of using an option because unknown options just trigger a warning would also work with attributes as long as you are willing to make Coq 8.11 a hard requirement for all your projects (which seems reasonable given the versions available in Ubuntu LTS and Debian reported by Paolo just above): https://github.com/coq/coq/pull/10997
Théo Zimmermann (May 12 2022 at 08:11):This warning is fatal by default, but you can locally disable it since it's a warning.
Théo Zimmermann (May 12 2022 at 08:12): Pierre-Marie Pédrot (May 12 2022 at 08:24):My point was exactly what Théo said, i.e. unset unknown attribute fatality.
Ali Caglayan (May 19 2022 at 10:38):on bedrock2
Ali Caglayan (May 19 2022 at 13:34):I've updated the list and it has grown
Maxime Dénès (May 20 2022 at 11:57):Incidentally, it seems the implementation of this warning makes elaboration of attributes depend on the logical environment, doesn't it?
Maxime Dénès (May 20 2022 at 11:57):I hit it in my parsing / execution separation branch
Maxime Dénès (May 20 2022 at 11:59):(it is because the only way to know if a section is open currently seems to be by asking the kernel, but this warning wants to do it more or less at parsing time, if you consider attribute elaboration being part of parsing)
Ali Caglayan (May 20 2022 at 12:43):Can we not simply lex the file and check if a section is open? I don't know about Undo tho.
Maxime Dénès (May 20 2022 at 13:07):Undo is only about tactics IIRC
Maxime Dénès (May 20 2022 at 13:08):I believe Lib used to have the right information about sections, but it was moved to the kernel
Ali Caglayan (Jul 30 2022 at 14:54):@Pierre-Marie Pédrot I see that there has been a lot of progress recently. What are we waiting for with fiat parsers and engine bench?
Pierre-Marie Pédrot (Jul 30 2022 at 16:51):I've just written an overlay for fiat-parsers today, but it's breaking backwards compat so it'll need some tweak. Same problem for engine-bench, @Jason Gross wants it to be backwards compatible with quite old versions.
Last updated: Dec 06 2023 at 14:01 UTC