Stream: Coq users

Topic: Notation for Explicit Arrays

view this post on Zulip Quentin Canu (Mar 13 2023 at 15:30):

Hello
I am currently trying to test some functions on persistent arrays from PArray.
I already used notations of form [| true; true | false|], but it is seems to not behave well with others modules that I import. My question is where can I find informations about the [| ... | ... |] notation. I don't find it anywhere in the documentation.

view this post on Zulip Gaëtan Gilbert (Mar 13 2023 at 15:37):

it's part of the basic term syntax https://coq.github.io/doc/master/refman/language/core/basic.html#grammar-token-term0
it seems not documented other than that (?)

view this post on Zulip Pierre Roux (Mar 13 2023 at 17:22):

Quentin Canu said:

it is seems to not behave well with others modules that I import

Could you be more precise? that might be a bug.

view this post on Zulip Quentin Canu (Mar 14 2023 at 08:30):

In my case, it is BigQ from the bignums library

view this post on Zulip Pierre Roux (Mar 14 2023 at 08:32):

@Quentin Canu I mean: would you have an example where "it does not behave well". If it's a bug in either PArray or bignums, I'd like to fix it.

view this post on Zulip Quentin Canu (Mar 14 2023 at 08:36):

Require Import PArray Uint63.

Check [|true; true | false|].

From Bignums Require Import BigQ.

Check [|true; true | false|].

The last line fails in my case

view this post on Zulip Pierre Roux (Mar 14 2023 at 08:56):

That indeed looks like a bug in bignums, thanks

view this post on Zulip Pierre Roux (Mar 14 2023 at 09:30):

So, I fixed the bug in bignums master branch by changing the problematic [_] notation to `[_] but I'm still wondering what is the best strategy to publish the fix (I'm leaning toward publishing a coq-bignums.8.17.1, as well as 8.13.1,...,8.16.1 but that might break a few packages and OPAM files may have to be adjusted).

view this post on Zulip Gaëtan Gilbert (Mar 14 2023 at 10:00):

isn't it a coq bug? I get an error with 

Require Import List.
Import ListNotations.
Check [| true; true | false |].

too (Error: Syntax error: [term level 200] expected after '[' (in [term]).)

view this post on Zulip Pierre Roux (Mar 14 2023 at 10:13):

We could consider that a Coq bug too but I don't know how to fix it then. (and ListNotations is well known to be troublesome, that's why it is in a module in the first place I guess)

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:03):

OTOH if some code doesn't work with ListNotations it could as well not exist for many users...

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:24):

okay, so [| true; true | false |] is undocumented primitive syntax which isn't even notation for something else? I can't get Set Printing All to desugar it...

view this post on Zulip Gaëtan Gilbert (Mar 14 2023 at 12:27):

yes

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:30):

honestly, I'd still consider dropping it, and requiring replacements to be opt-in and compatible with ListNotations.

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:37):

Of course, that violates normal compatibility policies and might be impractical; it just seems a problem that this was merged in the first place.

view this post on Zulip Gaëtan Gilbert (Mar 14 2023 at 12:38):

I don't think we realised that it's incompatible

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:40):

sure, I was not suggesting you were torturers. More constructively, "any new syntax must be tested together with _all_ stdlib notation modules" might belong in the MR review checklist

view this post on Zulip Pierre Roux (Mar 14 2023 at 12:40):

It's not exactly undocumented as noted by Gaëtan in the second message of this thread but it's indeed a primitive syntax.

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:41):

I've read that message, and I'm choosing "undocumented" as more accurate than "documented"

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:45):

I might have unreasonable expectations here, but I'd like at least to not blame ListNotations for this.

More concretely, I'm not sure BigNums deserves blame either but I'm not familiar with it.

view this post on Zulip Pierre Roux (Mar 14 2023 at 12:45):

I'd consider BigNums as to blame here (I'm saying that as a maintainer ;) )

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:45):

(and to be clear I have nothing against PArray _users_)

view this post on Zulip Pierre Roux (Mar 14 2023 at 12:47):

Besides, the doc for ListNotations (see the comment just above the Module opening) reads "Standard notations for lists. In a special module to avoid conflicts."

view this post on Zulip Pierre Roux (Mar 14 2023 at 12:48):

I understand that as some acknowledgment that this notation can be problematic, hence it's isolation in a module, that's not loaded by default.

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:51):

that's a good question, and I might be biased because stdpp exports ListNotations by default, but it seems almost any Coq notation can be problematic (that's fundamental to LL(1) parsing), and some other stdlib modules follow the same convention

view this post on Zulip Paolo Giarrusso (Mar 14 2023 at 12:57):

OTOH to be perfectly honest I should admit that, contrary to what I expected,mathcomp/ssreflect/seq.v keeps building even when plugging Require Import PArray. in.

view this post on Zulip Pierre Roux (Mar 14 2023 at 12:58):

See https://github.com/coq/coq/commit/d068a422173a55eda92996aa46ec1094be614520 for the history

view this post on Zulip Pierre Roux (Mar 14 2023 at 12:59):

Paolo Giarrusso said:

OTOH to be perfectly honest I should admit that, contrary to what I expected,mathcomp/ssreflect/seq.v keeps building even when plugging Require Import PArray. in.

Yes, mathcomp has its own list notation with an additional :: (i.e., [:: 1; 2; 3] instead of [1; 2. 3]) probably for good reasons.

view this post on Zulip Gaëtan Gilbert (Mar 14 2023 at 13:22):

Paolo Giarrusso said:

OTOH to be perfectly honest I should admit that, contrary to what I expected,mathcomp/ssreflect/seq.v keeps building even when plugging Require Import PArray. in.

why wouldn't it? even if it used [] notations instead of [::]

view this post on Zulip Gaëtan Gilbert (Mar 14 2023 at 13:23):

Pierre Roux said:

See https://github.com/coq/coq/commit/d068a422173a55eda92996aa46ec1094be614520 for the history

BTW that commit says "bug 2463" but it seems to actually be https://github.com/coq/coq/issues/2438

view this post on Zulip Pierre Roux (Mar 14 2023 at 15:20):

FYI, regarding bignums, we discussed the matter with @Erik Martin-Dorel (comaintainer) and came up with the following path of actions: https://github.com/coq-community/bignums/pull/73#issuecomment-1468302491

view this post on Zulip Quentin Canu (Mar 14 2023 at 15:57):

Thank you, I'll have a look on it

view this post on Zulip Pierre Roux (Mar 16 2023 at 07:19):

@Quentin Canu there is a discussion about the update of the Docker images, could you express your opinion i any there: https://github.com/coq/opam-coq-archive/pull/2505

view this post on Zulip Pierre Roux (Mar 20 2023 at 09:25):

@Quentin Canu so if you use OPAM you should now be able to opam update then opam install coq-bignums.9.0.0+coq8.16 to get the fixed bignums without the conflicting notation.

view this post on Zulip Pierre Roux (Mar 20 2023 at 09:26):

BTW, if you happen to develop a refinement with arrays, please consider submiting a pull request on CoqEAL, this is definitely something missing there.

Last updated: Oct 04 2023 at 22:01 UTC