Jason Gross

`git clone` can fail in confusing ways if a repository is set up to use `git lfs` but `git lfs` is not installed / initialized. It would be nice to...

[feature] minimizer should support regression minimization

1

When reporting regressions (e.g., https://github.com/rocq-prover/rocq/issues/20938 if it weren't already minimized), it would be nice to be able to tag the bot and ask it to minimize against two versions of...

st.lists rejects too much when generating large lists

2

Consider this code: ```python from hypothesis import given, strategies as st, seed @st.composite def biglist(draw, strat): N = draw(st.integers(min_value=1, max_value=20000)) N = min(8192, N) return draw(st.lists(strat, min_size=N, max_size=N)) @seed(195400164800693954998404088135293827994) @given(biglist(st.floats(allow_nan=False,...

performance of run_state_machine_as_test drops drastically as a function of the number of state machine rules

3

Here's a synthetic example demonstrating the performance issue: ```python #!/usr/bin/env python import time import operator import hypothesis.strategies as st from hypothesis import settings, Verbosity from hypothesis.stateful import ( Bundle, RuleBasedStateMachine,...

Move baseof.html to layouts/_default directory

1

Relocate baseof.html to follow Hugo's standard layout structure convention.

conversion fails to reduce enough in the presence of sprop

4

### Description of the problem I am not sure if this is a bug with rocq-lean-import or with Rocq, cf https://github.com/rocq-community/rocq-lean-import/issues/45#issuecomment-3565927116 [pnni.txt](https://github.com/user-attachments/files/23687488/pnni.txt) ### Small Rocq / Coq file to reproduce...

Checking Inductive/Variant/CoInductive from Ltac2

1

### Is your feature request related to a problem? How do I determine whether an `inductive` is an `Inductive` or `CoInductive` (or non-recursive / `Variant`) from Ltac2? ### Proposed solution...

only printing notations should never have level clashes

1

#### Description of the problem I think this should work. @herbelin , do you agree? ```coq Axiom funspec : forall {A B} T (pre : T -> A) (post :...

Ltac2: deprecate the current implementation of `refine` in favor of `unshelve eexact`?

8

As I understand it, `Control.refine f` and `Control.unshelve (fun () => let c := f () in eexact $f)` should have the same behavior modulo side-condition ordering. Today I have...

(transparent_)abstract in tactics in terms should not inline

8

#### Version 8.8.0 #### Description of the problem This is wrong: ```coq Check ltac:(refine (_ : Z); transparent_abstract (exact 1)). (* let Top_anonymous_subterm := 1 in Top_anonymous_subterm : Z *)...