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.


Last updated: Aug 11 2022 at 02:03 UTC