Tify + lra solves programs mixing Z and R

[fajb]

This PR makes substantial changes to lra so that is can handle Mixed Integer Linear Programs (MILP) i.e. goals where variables range over either R or Z.

This requires several changes (see also PR rocq-prover/stdlib#110).

• tify T generalises zify and takes as argument the type T the goal is translated to.
  As a result, zify is now simply tify Z
  (The user facing interface is unchanged except that Zify commands are deprecated and renamed into Tify)
• tify R maps a goal towards Z and adds isZ predicates that needs to be exploited by lra.
• To solve MILP, we adapt the lia code and perform integer reasoning only when the relevant variables range over the integers.
• As a side-effect, this requires a direct handling of strict constraints >. To do so, the simplex code is adapted to manipulate symbolic infinitesimals. The rough idea is that a strict constraint c > 0 can be intepreted as (c - $\epsilon$ >= 0)

Much testing is needed to ensure the absence of regressions.

• Added / updated test-suite.

• Added changelog.

• Added / updated documentation.

  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

[proux01]

Définitely not 9.0.0 material (now that we have the rc, only bugfixes and doc improvements should go there)

[fajb]

Définitely not 9.0.0 material (now that we have the rc, only bugfixes and doc improvements should go there)

I agree! I never know where we are in the release cycle.

[proux01]

No worries (and if you want to remember: basically this kind of nice/feature change should always get the next available "X.Y+rc1" milestone)

[fajb]

@coqbot: run CI

[proux01]

@fajb if you want to run the full CI nowadays you need to ask @coqbot run full CI (or put the request: full CI label before pushing)

[fajb]

@coqbot: run full CI

[fajb]

@fajb if you want to run the full CI nowadays you need to ask @coqbot run full CI (or put the request: full CI label before pushing)

I have just seen that! Thanks.

[coqbot-app]

🔴 CI failures at commit 10d6df4 without any failure in the test-suite

✔️ Corresponding jobs for the base commit ff34785 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-stdlib, ci-stdlib

• You can also pass me a specific list of targets to minimize as arguments.

[andres-erbsen]

@coqbot run full ci

I just chatted with an user eagerly awaiting this feature at HACS.

[fajb]

Hi @andres-erbsen, good to know this is an interesting feature.

Actually, I need help to run the CI.
Though, I think I added an overlay for the stdlib, it seems the CI tries to compile with the current stdlib. That's not going to work,

Also, the change is substantial; cleanup and testing is needed...

[SkySkimmer]

CI is getting the overlay commit AFAICT https://gitlab.inria.fr/coq/coq/-/jobs/5517508#L1430

+ git log -n 1 'HEAD^2'
commit fe6b078668992a4ec99eeafd34a7ba17f1b04c0b
Author: Frédéric Besson <[email protected]>
Date:   Thu Feb 27 10:57:05 2025 +0100
    [Cos_rel] drop dependency on Lra
    
    lra, nra -> field,ring
+ git log -n 1
commit 0d278af464a1ba1daf6068cf2c964c2362602779 (HEAD -> master)
Merge: e19046a fe6b078
Author: Nobody <[email protected]>
Date:   Tue Mar 25 14:08:46 2025 +0000
    Merge branch 'rify' of https://github.com/fajb/stdlib

[coqbot-app]

🔴 CI failures at commit ac7d358 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 582c03b succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-coqprime, ci-lean_importer, ci-smtcoq, ci-smtcoq_trakt, ci-stdlib_test

• You can also pass me a specific list of targets to minimize as arguments.

[fajb]

CI is getting the overlay commit AFAICT https://gitlab.inria.fr/coq/coq/-/jobs/5517508#L1430

Good. And for some reason, the CI goes further than my previous attempt.

[coqbot-app]

🔴 CI failures at commit b1aa3a2 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 7f8da07 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-stdlib, ci-stdlib

• You can also pass me a specific list of targets to minimize as arguments.

[fajb]

@coqbot run full ci

[coqbot-app]

🔴 CI failures at commit de5a6d9 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 7f8da07 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-stdlib, ci-stdlib

• You can also pass me a specific list of targets to minimize as arguments.

[fajb]

I am confused. It seems the CI turns deprecation messages into errors...
That looks inconvenient...

[proux01]

I am confused. It seems the CI turns deprecation messages into errors... That looks inconvenient...

I guess you mean in Stdlib? Indeed, that's bad as it forces Coq developers to handle new warnings immediatly in the library, whereas this should be done by library developers at their own pace. You can probably fix it by replacing this line

rocq/dev/ci/scripts/ci-stdlib.sh

Line 13 in a09cdd9

dev/with-rocq-wrap.sh dune build --root . --only-packages=rocq-stdlib @install

with

  dev/with-rocq-wrap.sh dune build --root . -p rocq-stdlib @install

And we should add a CI job in Stdlib repo checking for absence of warnings when compiling on last stable Rocq.

[SkySkimmer]

Do not use -p, it interacts badly with caching in my experience.

[proux01]

Maybe --profile release or something like that (or simply replace the whole thing with make)

[Zimmi48]

Maybe --profile release or something like that (or simply replace the whole thing with make)

-p just means --profile release.

It's a bad practice to use it when developing a library, but why would it be a problem when testing the Stdlib in our CI?

That being said, what I would recommend is just for the Stdlib to selectively configure which deprecation warning are temporarily hidden.

[SkySkimmer]

-p means --release not -profile release
--release also includes --no-config which means it can disable the cache, and some other stuff

[proux01]

So -profile release may be what we want (or again, just use make, at least it works)

That being said, what I would recommend is just for the Stdlib to selectively configure which deprecation warning are temporarily hidden.

Of course, but that's Stdlib developers' job, not core developers' one. And they probably want to do that regularly on a stable release, not continuously on master.

[haselwarter]

Does this need another full CI run before being considered for getting merged? The test suite seems to have run successfully.

[proux01]

According to the top message, it's still requires quite a bit of work.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app]

This PR was not rebased after 30 days despite the warning, it is now closed.

[haselwarter]

Is there an easy way to test this by setting up an opam switch that uses this PR for Rocq?