Kazuhiko Sakaguchi

icon indicating an email [email protected]

icon location Lyon, France icon location Postdoc in the Plume team at CNRS, ENS de Lyon, UCBL, LIP | Interests: interactive theorem proving, formalization of mathematics, and proof by reflection

Results 306 comments of Kazuhiko Sakaguchi

Put lemma-overloading back to CI

NixOS/nixpkgs#355908

Port to derive.param2 of Coq-Elpi

Surprisingly, it's still compatible with Coq 8.13 and MathComp 1.13, though a few docker-mathcomp images fail to install Coq-Elpi because of the version of OCaml they use (looks like the...

dune is pinned to non-existent versions

I have the same issue with Elpi in the `mathcomp/mathcomp:2.2.0-coq-8.19` and `mathcomp/mathcomp:2.3.0-coq-8.19` images. I think that the only robust solution is to add the `opam-repository-archive` repository, at least for old...

dune is pinned to non-existent versions

> You probably want to ask about unarchiving elpi too. Thank you. It worked: ocaml/opam-repository#28076.

adapt to MC#1256

~Re-running `mathcomp/mathcomp-dev:coq-8.18` just in case since it took 28 minutes.~ No, it took time just because of recompiling MathComp.

adapt to MC#1256

Thanks!

Bogus error: The conclusion of a builder is a mixin whose parameters

Fixed by #433?

Deprecating structures/mixins/factories

IMO, we unlikely want to remove a structure, but we may want to remove a factory in favor of another factory or mixin when we find the former useless.

Deprecating structures/mixins/factories

If Coq had a feature to deprecate a module, we wouldn't need this feature in HB: ``` #[deprecated(since="mathcomp 2.3.0")] Module hasRelativeComplement := BDistrLattice_hasSectionalComplement. ```

Review and remove the `HB.instance` declarations with ` #[warning="-HB.no-new-instance"]` attribute

Doing this clean-up before the propagation of p.z.-ring stuff (e.g., #1385) and semilinear stuff (e.g., #1269) would make the latter work (propagation) a little bit easier.