Stream: math-comp devs

Topic: Recommended way of using classic ssreflect from Coq

view this post on Zulip Karl Palmskog (Jul 02 2020 at 09:10):

There are many (older) Coq developments floating around that have Require Import ssreflect., but will not immediately work with the ssreflect bundled with Coq (although ssr has all they require). My goto solution has been to define a file with:

From Coq Require Export ssreflect.
Global Set SsrOldRewriteGoalsOrder.
Global Set Asymmetric Patterns.
Global Set Bullet Behavior "None".

... to get the old behavior. However, I have to duplicate this file in all projects. Is there any alternative to the duplication? Should something like this file live in Coq stdlib?

view this post on Zulip Enrico Tassi (Jul 02 2020 at 09:12):

I'm afraid the only alternative is From mathcomp Require Import ssreflect (which contains these lines IIRC).

view this post on Zulip Karl Palmskog (Jul 02 2020 at 09:13):

right, but then suddenly your project depends on coq-mathcomp-ssreflect. This is what I think should no longer be necessary, unless you actually use stuff outside of ssr (which many projects don't)

view this post on Zulip Karl Palmskog (Jul 02 2020 at 09:23):

@Enrico Tassi so I take it you don't think adding something like theories/ssr/compat.v with that content would be welcome among devs?

view this post on Zulip Enrico Tassi (Jul 02 2020 at 09:28):

I just don't see the usecase. If you were using ssr before the integration in Coq, you were already depending on coq-mathcomp-ssreflect. So adding a From mathcomp to your files does not seem a big change (and also using From seems to be the recommended way of importing these days).

Is there a scenario I don't see?

view this post on Zulip Karl Palmskog (Jul 02 2020 at 09:33):

There are many projects out there that only use the ssreflect proof language and nothing else from ssreflect. And they started using the proof language before the ssr integration in Coq, so they rely on the mathcomp behavior of the proof language. Now, why would those projects want to depend on coq-mathcomp-ssreflect? That's one more dependency in opam or Nix that you have to state and have users download every time. The only thing these projects get from coq-mathcomp-ssreflect is the above behavior automatically. One whole dependency is a quite a lot to pay for four lines of Vernac.

view this post on Zulip Enrico Tassi (Jul 02 2020 at 09:51):

I agree, I was just saying that this dependency was already there... I think you can propose the extra file, and see what others think. I don't see a big problem with such a file being there, maybe under a name that is more precise, eg ssreflect_v1_4 (I don't recall in which version it was merged, I would put there the one before) so that you can Require Import ssreflect_v1_4. rather than Require Import ssr.compat.

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 09:55):

I'd definitely recommend against Global Set and in favor of project-wide option setting through -set and coq_flags in Dune or -arg in coq_makefile / _CoqProject.

view this post on Zulip Karl Palmskog (Jul 02 2020 at 09:56):

Théo Zimmermann said:

I'd definitely recommend against Global Set and in favor of project-wide option setting through -set and coq_flags in Dune or -arg in coq_makefile / _CoqProject.

But then it should be done this way in MathComp too: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssreflect.v#L4 --- meaning every project using MathComp has to change its _CoqProject/Makefile?

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 09:56):

Sure! But this will be a breaking change (although a welcome one) for projects depending upon math-comp.

view this post on Zulip Karl Palmskog (Jul 02 2020 at 09:57):

and I guess this only works in 8.12?

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 09:57):

No, it is already supported at least in 8.11

view this post on Zulip Karl Palmskog (Jul 02 2020 at 09:57):

meaning it can only be done in like... 8.15

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 09:58):

Actually, it is supported since 8.10!

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 09:58):

https://coq.inria.fr/refman/changes.html#other-changes-in-8-10-beta1

view this post on Zulip Enrico Tassi (Jul 02 2020 at 09:59):

Passing -arg is better w.r.t. "virality" but does not solve the original problem which is "not to have these options set in each and every project".

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 09:59):

Sure, but at least, it is less invasive since you don't have to create a Coq file that you import everywhere.

view this post on Zulip Karl Palmskog (Jul 02 2020 at 10:00):

right, it is an improvement for sure for projects that don't need Coq 8.9 or earlier

view this post on Zulip Enrico Tassi (Jul 02 2020 at 10:00):

I let @Karl Palmskog say what he prefers, to me it is less invasive to put one file in Coq, than 2 lines in each project using Coq

view this post on Zulip Enrico Tassi (Jul 02 2020 at 10:01):

(I've already proposed the solution I prefer, which is a dependency on the ssr package from MC)

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 10:02):

FTR with respect to the removal of Global Set from math-comp, there's also Export Set that is available since 8.8 and allows to reproduce the same behavior (from the point of view of reverse deps).

view this post on Zulip Pierre-Marie Pédrot (Jul 02 2020 at 10:02):

Note that instead of Global Set you can also go for Export Set, which is more modular.

view this post on Zulip Enrico Tassi (Jul 02 2020 at 10:02):

Nice, what is it's scope?

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 10:02):

You get the options if you Import directly the file that sets them.

view this post on Zulip Enrico Tassi (Jul 02 2020 at 10:02):

We want the option to be global WRT mathcomp, but not necessarily reach its users

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 10:03):

In fact, it might be time to deprecate Global Set in Coq.

view this post on Zulip Pierre-Marie Pédrot (Jul 02 2020 at 10:03):

Global Set can be used for nice hacks though

view this post on Zulip Pierre-Marie Pédrot (Jul 02 2020 at 10:03):

the fact it is highly non-recommended doesn't necessarily mean we should remove it

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 10:04):

OK maybe

view this post on Zulip Pierre-Marie Pédrot (Jul 02 2020 at 10:04):

(I think a warning would be nice though)

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 10:04):

Anyway, FWIW here is the documentation of locality attributes of Set / Unset: https://coq.github.io/doc/master/refman/language/core/basic.html#locality-attributes-supported-by-set-and-unset

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 10:05):

The warning that the manual contains could indeed become a warning that is raised when using the command with the Global / global attribute.

view this post on Zulip Karl Palmskog (Jul 02 2020 at 10:05):

for my use case, I guess -arg is enough, but I will have to test

view this post on Zulip Karl Palmskog (Jul 02 2020 at 16:27):

looks like the SsrOldRewriteGoalsOrder option is only available when a certain plugin is loaded:

let () =
  Goptions.(declare_bool_option
    { optkey   = ["SsrOldRewriteGoalsOrder"];

(in plugins/ssr/ssrequality.ml)

So the -set approach seemingly can't accomplish the same as Global Set here.

view this post on Zulip Théo Zimmermann (Jul 02 2020 at 16:59):

Good point. The argument approach allows one to load a plugin though (see -rfrom / -rifrom flags and also the 8.12 changes related to the interleaving of command-line flags, second bullet at https://coq.github.io/doc/master/refman/changes.html#tools).

Last updated: Oct 13 2024 at 01:02 UTC