Jason Gross

@coqbot bench

@coqbot bench

@coqbot run full ci

I tensed through the web interface by temporarily enabling it @coqbot bench

Can we (a) check the size reduction in .vo size across the entire CI somehow, and (b) get monogram statistics for the bytecode words across the entire CI so that...

How much trouble would it be to support both sorts of closure compilation schemes? It would be nice to be able to manually annotate some definitions as "symbolic-like closures".

> What to do about this? Do we consider for coqide that putting a breakpoint is enough and, in vscoq/coq-lsp, that hovering will eventually display the goals in the middle...

> > with the printing done in one go? > > Yes. Only one call to Feedback.msg_notice. This is also possible in Ltac2, right? Map over Control.hyps, building a message...

> Can somebody confirm it's a bug and that this is the morally expected behaviour of `Scheme Elimination`? I confirm this is a bug, and the documentation agrees that it's...

That is not the issue. The issue is that it depends on a LaTeX package that isn't a dependency of hevea, and thus fails even when hevea and LaTeX are...