Stream: math-comp users

Topic: Require Import mathcomp.ssreflect.ssreflect.


view this post on Zulip Karl Palmskog (Mar 11 2022 at 09:50):

Is there any reason anymore for having

Require Import mathcomp.ssreflect.ssreflect.

instead of

From mathcomp Require Import ssreflect.

anymore?

(Case in point: fourcolor, which has the former idiom almost everywhere)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 11 2022 at 09:53):

Karl Palmskog said:

Is there any reason anymore for having

Require Import mathcomp.ssreflect.ssreflect.

instead of

From mathcomp Require Import ssreflect.

anymore?

(Case in point: fourcolor, which has the former idiom almost everywhere)

I think there was one in the past, but likely not valid anymore

view this post on Zulip Karl Palmskog (Mar 11 2022 at 09:55):

OK, but then at what MC version did it cease to be relevant? fourcolor is compatible with 1.11 and later, which should not need it, right?

view this post on Zulip Janno (Mar 11 2022 at 09:56):

Is it no longer true that the second one is ambiguous if there are multiple module files called ssreflect in the library? Maybe I am misremembering.

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 10:25):

@Janno Yes, but the first one is globally ambiguous, which is worse.

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 10:26):

The first matches any path *.mathcomp.ssreflect.ssreflect while the second matches mathcomp.*.ssreflect

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 10:27):

so if somebody out there in your Coq install has a mathcomp submodule you may pick it up with the first one, but not with the second one

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 10:27):

so the second one has a good locality property, i.e. it's the responsibility of the library author not to name two files identically

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 10:29):

I think we should recommend as good practice to have From clauses everywhere except for your local files.

view this post on Zulip Théo Winterhalter (Mar 11 2022 at 10:30):

Pierre-Marie Pédrot said:

I think we should recommend as good practice to have From clauses everywhere except for your local files.

Is it bad to also use it for local files?

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 10:31):

It's not bad but if you add all external libraries through -Q it shouldn't matter

view this post on Zulip Pierre-Marie Pédrot (Mar 11 2022 at 10:32):

(i.e. it's a convenience to write shorter names)

view this post on Zulip Cyril Cohen (Mar 11 2022 at 11:51):

The historical reason was not a matter of ambiguity but of backward compatibility: at some point several years ago, when ssr was not yet in Coq, we used to add some missing support in the ssreflect.ml file so that From was recognized, so we started by importing the absolute (logical) path of just ssrelflect.v so that subsequent From directives were correctly used accross coqc/coqtop/coqdoc.
This is an oddity that should be removed now.

view this post on Zulip Cyril Cohen (Mar 11 2022 at 11:54):

So it ceased to be relevant either when From was properly supported everywhere (coqc/coqtop/coqdoc) or when ssreflect was merged into Coq... which were both way way before coq 8.11

view this post on Zulip Karl Palmskog (Mar 11 2022 at 11:55):

so we should consistently use From mathcomp Require Import ssreflect. now? Or some other From variant?

view this post on Zulip Cyril Cohen (Mar 11 2022 at 11:56):

Yes From mathcomp Require Import ssreflect ssrfun ssrbool. when being selective of From mathcomp Require Import all_ssreflect. otherwise.

view this post on Zulip Cyril Cohen (Mar 11 2022 at 11:57):

(Never import ssreflect without ssrfun and ssrbool, and never use the Coq one's directly)

view this post on Zulip Paolo Giarrusso (Mar 11 2022 at 15:17):

Pierre-Marie Pédrot said:

The first matches any path *.mathcomp.ssreflect.ssreflect while the second matches mathcomp.*.ssreflect

Is that still true if you don't use -R (outside maybe math-comp itself?) That's what you seem to imply with

Pierre-Marie Pédrot said:

It's not bad but if you add all external libraries through -Q it shouldn't matter

view this post on Zulip Karl Palmskog (Mar 11 2022 at 20:05):

based on Cyril's recommendations, I did https://github.com/coq-community/fourcolor/pull/40


Last updated: Feb 08 2023 at 04:04 UTC