Jason Gross

v3 regression over v2: `opam exec` now fails with "Exec format error" on shell scripts on Windows

2

``` opam exec -- ./test.sh Fatal error: exception C:\hostedtoolcache\windows\opam\2.2.1\x86_64\opam.exe: "create_process" failed on ./test.sh: Exec format error ``` https://github.com/JasonGross/test/actions/runs/10953316111/job/30413386004 [logs_28625164728.zip](https://github.com/user-attachments/files/17069974/logs_28625164728.zip) Full yml file ```yaml name: Example Workflow on: [push, pull_request] jobs:...

Would it be possible to tag a version compatible with Coq 8.17 and release it on opam? I'm trying to minimize https://github.com/MetaCoq/metacoq/issues/1072 with the bug minimizer, and it seems there...

Login fails when voice id is pending activation

1

If Voice ID is partially set up, the login page redirects to https://client.schwab.com/service/forms/VoiceBiometric instead of whichever page was selected:  The relevant HTML fragment for clicking "Cancel", which just skips...

Target minimal changes in proof / goal outputs with `--minimize-for-first-proof-diff`

1

Extend the minimizer with a `--minimize-for-first-proof-diff` which can (a) insert `Show.` between every statement in the proof, and (b) replace `;` with `. all:`. Then it can look for the...

In preparation for threading them through more explicitly.

the minimizer should support --coqlib and --passing-coqlib explicitly, and thread through these arguments

1

To work around things like https://github.com/coq/coq/issues/20129 and https://github.com/coq/coq/issues/20128 and https://github.com/coq/coq/pull/20101#issuecomment-2611988918

The general problem with .v and .glob files having the same time is that we can't tell whether the .v file has been updated since the .glob file was generated....

Nearly complete work for handling #223 Still todo: - [ ] don't automatically add `-Q . Top` or w/e - [ ] fix handling of lib_of_filename around `clear_libimport_cache(lib_of_filename(output_file_name, **kwargs))` -...