Karl Palmskog (Mar 11 2022 at 09:50): 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)
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
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?
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.
Pierre-Marie Pédrot (Mar 11 2022 at 10:25):@Janno Yes, but the first one is globally ambiguous, which is worse.
Pierre-Marie Pédrot (Mar 11 2022 at 10:26):The first matches any path *.mathcomp.ssreflect.ssreflect while the second matches mathcomp.*.ssreflect
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
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
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.
Théo Winterhalter (Mar 11 2022 at 10:30):Pierre-Marie Pédrot said:
I think we should recommend as good practice to have
Fromclauses everywhere except for your local files.
Is it bad to also use it for local files?
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
Pierre-Marie Pédrot (Mar 11 2022 at 10:32):(i.e. it's a convenience to write shorter names)
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.
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
Karl Palmskog (Mar 11 2022 at 11:55):so we should consistently use From mathcomp Require Import ssreflect. now? Or some other From variant?
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.
Cyril Cohen (Mar 11 2022 at 11:57):(Never import ssreflect without ssrfun and ssrbool, and never use the Coq one's directly)
Paolo Giarrusso (Mar 11 2022 at 15:17):Pierre-Marie Pédrot said:
The first matches any path
*.mathcomp.ssreflect.ssreflectwhile the second matchesmathcomp.*.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
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: Apr 18 2024 at 16:01 UTC