Stream: math-comp devs

Topic: ✔ Strange error with finmap

view this post on Zulip Julien Puydt (May 24 2022 at 06:41):

After recompiling Debian packages to avoid "inconsistent assumptions" errors, I'm having issues with finmap: From mathcomp Require Import finmap. triggers an error:

Error:
Level 2 is already declared right associative while it is now expected to be left associative.

and I have no clue what it means...

view this post on Zulip Karl Palmskog (May 24 2022 at 06:44):

just doing From X Require Import Y. in a file is not guaranteed to work, for any Coq project. It depends on what you have loaded previously

view this post on Zulip Karl Palmskog (May 24 2022 at 06:45):

so I'm guessing this is some custom file that has Require-Imports above it?

view this post on Zulip Julien Puydt (May 24 2022 at 06:45):

It's a test of loading, so the file is only the line I gave.

view this post on Zulip Julien Puydt (May 24 2022 at 06:47):

Ah, From mathcomp.finmap Require Import multiset. works.

view this post on Zulip Julien Puydt (May 24 2022 at 06:47):

So does From mathcomp.finmap Require Import set..

view this post on Zulip Karl Palmskog (May 24 2022 at 06:48):

did you reproduce on pure opam installation? Works fine for me on coq-mathcomp-finmap.dev

view this post on Zulip Julien Puydt (May 24 2022 at 07:15):

I don't have opam.

view this post on Zulip Ana de Almeida Borges (May 24 2022 at 10:20):

This happens when you import finmap without importing ssrfun first. In general mathcomp stuff should only be imported after ssreflect ssrbool ssrfun are imported.

view this post on Zulip Julien Puydt (May 24 2022 at 12:24):

Excellent! That was it... thanks!

view this post on Zulip Notification Bot (May 24 2022 at 12:24):

Julien Puydt has marked this topic as resolved.

view this post on Zulip Julien Puydt (May 24 2022 at 12:59):

(Though I still wonder why @Karl Palmskog didn't see it, and I wonder if finmap hence shouldn't import what it needs beforehand.)

view this post on Zulip Ana de Almeida Borges (May 24 2022 at 13:20):

Yeah, I have no idea and I also wonder.

view this post on Zulip Karl Palmskog (May 24 2022 at 13:31):

I tried in both ProofGeneral/Emacs and coqc with the dev/repo version of finmap. Maybe someone wants to try a naked From mathcomp Require Import finmap. on Nix. Or maybe only finmap 1.5.1 and below has this behavior? The release is about 1.5 years old at this point.

Last updated: Dec 07 2023 at 09:01 UTC