Jason Gross

@coqbot CI minimize ci-metacoq

@coqbot ci minimize

@coqbot ci minimize

@SkySkimmer Do you know what's going on with the 404 from https://gitlab.inria.fr/coq/coq/-/jobs/5509295/artifacts/download / why the bot is sending the minimizer a non-existent url for unimath?

Hm, maybe skipping the build of passing coqc will work just fine, since we absolutize requires very early. @coqbot ci minimize

> Hm, maybe skipping the build of passing coqc will work just fine, since we absolutize requires very early. Seems to be working

That's the first one, the second one is still running. The confusion with the metacoq log is that make seems to be run with -j so the actual error is...

> do you know why "could not inline MetaCoq.PCUIC.Syntax.PCUICOnFreeVars" The error message shifted from File "./theories/PCUICWellScopedCumulativity.v", line 419, characters 0-4: Error: (in proof into_ws_cumul_decls): Attempt to save an incomplete proof...

> 3\. Do what is being done in [fiat/src/Common/Wf1.v](https://github.com/mit-plv/fiat/blob/4063f04f5c3605ad06b8a476e2300505cab1ca5d/src/Common/Wf1.v#L313). I don't know exactly what is going on there, but it looks like it solves this problem? > > > I...

> ??? cc @JasonGross Somehow the minimizer runner thinks the arguments to coq are `"-native-output-dir" "-native-compiler" "on"`. Is this right or is there some missing argument? Also, why does the...