coq-tools

coq-tools copied to clipboard

This issue lists Renovate updates and detected dependencies. Read the [Dependency Dashboard](https://docs.renovatebot.com/key-concepts/dashboard/) docs to learn more.[View this repository on the Mend.io Web Portal](https://developer.mend.io/github/JasonGross/coq-tools). This repository currently has no open or...

renovate[bot]

Figure out how to support import categories and comments in Require statements

1

The code at https://github.com/JasonGross/coq-tools/blob/9b3989871caa1315854a196f195ab2e4ce1a0c48/import_util.py#L220-L235 does not support comments in `From ... Require ...` statements. The code at https://github.com/JasonGross/coq-tools/blob/9b3989871caa1315854a196f195ab2e4ce1a0c48/find-bug.py#L822-L829 does not support import categories (https://github.com/coq/coq/pull/14892) nor filtered imports. Neither supports attributes...

JasonGross

Incremental compilation

5

It would be nice to have a mode where we kept a pool of coqtop workers and used `BackTo` to allow us to try multiple changes without recompiling the initial...

JasonGross

Tooling integration?

17

Hi, I am opening this issue to discuss some potential integration of these tools with some other existing tooling that could improve maintenance and functionality. In particular, I think that...

ejgallego

Remove every command which fails after removing the `Section`

1

> Could you remove every command which fails after removing the `Section`? ie > > * try removing Section > > * End fails, remove End > * success This...

JasonGross

[enhancement] Handle `Equations`

2

It would be nice to handle the following constructs: ```coq Equations isws_cumul_pb_fix_bodies (fk : fix_kind) (Γ : context) (idx : nat) (mfix1 mfix2 : mfixpoint term) (π : stack) (h...

JasonGross

Support selectively avoiding inlining modules

1

To work around https://github.com/coq/coq/issues/17968, it would be nice to support things like `--no-inline-module-regexp '^Ltac2\..*'` or `--no-inline-modules-under Ltac2`, maybe also `--no-inline-module Ltac2.Ltac` for exact matching as well.

JasonGross

(meanwhile opaque constraints could be turned into `Module Foo. Include constraint. End Foo.` or removed) _Originally posted by @SkySkimmer in https://github.com/JasonGross/coq-tools/issues/148#issuecomment-1472250687_

JasonGross

Minimizer: try to replace `Proof term.` with `Admitted.`

1

as in ~~~coq Lemma foo : nat. Proof 0. ~~~

SkySkimmer

Minimizer: try to split <+ into Include

1

Typically `Module Foo args := A

SkySkimmer