Hi all, I am attempting to use metacoq on unimath but it is conflicting on notations

This topic was moved here from #Coq users > Metacoq notations by Karl Palmskog.

not sure how to solve this, but you might want to post a minimal example with `Require Import <UniMath modules>. Require Import <MetaCoq modules>.`

that gives an error that devs can look at

here are the first one conflicting

Notation "X <- Y" := (Y -> X) (at level 90, only parsing, left associativity) : type_scope.

from https://github.com/UniMath/UniMath/blob/4a224a3b45428b6e4fc79fb53b250baf3df8ecfa/UniMath/Foundations/Init.v#L23 so that creates a scope in unimath.

```
File "./UniMath/Foundations/Init.v", line 26, characters 0-91: Error:
Level 90 is already declared to have right associativity while it is now expected to have\ left associativity.
```

that is when I put it back in. https://github.com/meta-introspector/UniMath/tree/hack/hack here is the code that is hacked to compile with metacoq so i commented out the parts of unimath that conflicted

Here is the notation of metacoq `Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2)) (at level 100, c1 at next level, right associativity) : monad_scope.`

from metacoq/utils/theories/monad_utils.v https://github.com/MetaCoq/metacoq/blob/ceda84e2dcac4ebb322438fdb0865782cd992ca2/utils/theories/monad_utils.v#L4

https://github.com/meta-introspector/metacoq/pull/1 ok i am starting to rework metacoq to use <-- for <- and ;;; for ;; to start with

honestly I think Unimath needs to bend instead because it came afterwards, metacoq is so hard to work with to make changes to it i will leave it.

https://github.com/UniMath/UniMath/pull/1825 here are my changes of the first 3 modules to replace the notations. First version of unimath compiled on top of metacoq

The changes are to the following notations

,, → ,,m

× → ×u

<- → <--

Also there was another change tpair takes only 2 args not 3

I did only up to Combinatorics for our purposes that should be enough

I got it working, https://twitter.com/introsp3ctor/status/1747358801106235687?t=tpqowEH13bL50IrmlX-gKA&s=19 have now unimath extracted to ocaml extracted to ppxlib

if you want to serialize anything in Coq, Serlib (part of SerAPI) is the recommended way

UniMath by design replaces the stdlib, so I wouldn't expect it to be compatible with stdlib cliets like MetaCoq. It also builds with flags like `-noinit -indices-matter -type-in-type`

.

Serlib is to my knowledge independent of Stdlib (although some tools on top of it may not be). It does low-level serialization of Coq data structures, including terms, built on ppx.

ah, you mean compatibility in the sense of using both MetaCoq and UniMath. I agree, they probably are very difficult to use together. But it should at least be possible to `Require`

both.

Aah, had to click on the tweet, now I get Karl's reply :smile:

ok i am back to working on it, now I extracted the ocaml back into coq using coq-of-ocaml, now i am working on using metacoq with unimath some more. https://github.com/coq/coq/issues/18567 i got coq to crash :)

It looks like serapi is being used to train ML models already that is good

Trying serlib out on master branch of unimath gives me this after a short run ```
Error: File "UniMath/Foundations/PartA.v", line 968, characters 16-17
In environment X : UU
P : X → UU
Q : X → UU
The term "P" has type "X → UU" while it is expected to have type
"∏ x : X, ?P x" (unable to find a well-typed instantiation for
"?P": cannot ensure that "X → Type" is a subtype of "X → UU").
```

so maybe it will need some massage there too. :/

sounds like type-in-type isn't on?

let me see, also "Definition UU := Type." is there in the Preample.v

are you using serlib via `sertop`

? There is also `sercomp`

for serializing whole files in one go (both come with the opam package `coq-serapi`

)

may also be worth taking a look at `fcc`

CLI tool that is developed in https://github.com/ejgallego/coq-lsp - it also uses serlib and provides some serialization options I believe

https://github.com/UniMath/UniMath/issues/554 so they say that type in type is not enabled yet. running like this ```
sercomp --input=vernac --mode=sexp -R UniMath/Foundations/,UniMath.Foundations \
$1 > $1.secp
```

yes i was thinking about going to lsp or semgrep next

you need multiple `-R`

clauses

yes for more subdirs later, but this is all just in foundation right now

they say that type in type is not enabled yet

no, unimath uses type-in-type globally

ok let me look again, honestly i dont know what it is yet :)

I don't think we have a type-in-type option for `sercomp`

, but probably it could be added by doing some OCaml changes (the whole of `sercomp`

is just a thin layer on top of Serlib and Coq's API)

yes, ok. https://github.com/UniMath/UniMath/issues/648 here they have ideas to turn UU into a notation. Lots of fun.

but i got this to serialize via metacoq, even if the results were not perfect

for example, here is a PR adding support for `impredicative-set`

: https://github.com/ejgallego/coq-serapi/commit/4fb4e6b2d032b6d2ee09984de0876a6be636a21a

Thanks but that will be a little over my head right now, still struggling with basics :)

i have sexp for some of the files to consider now at least. will try lsp next

Karl Palmskog said:

I don't think we have a type-in-type option for

`sercomp`

, but probably it could be added by doing some OCaml changes (the whole of`sercomp`

is just a thin layer on top of Serlib and Coq's API)

for unimath you can put `Global Unset Universe Checking.`

at the beginning of the first file and it should work

Wow that worked, I needed to add it to each file with the error but great job thank you!

https://github.com/meta-introspector/UniMath/pull/7/files here is the new rebase on master that has the changes for Foundation, will do a bit more and that is a good data source

this is resistant to the other fix

```
ine 566, characters 18-28
In environment
X : gr
Y : subgr X
x1 : X
x2 : X
The term "grinv X x1" has type "pr\
1hSet X"
while it is expected to have type \
"Type".```
```

```
ory/AffineLine.v", line 214, characters 8\6-87
In environment
P : ℤ → Type z : ℤ
The term "1" has type "pr1hSet hz"\
while it is expected to have type
"Type".``` i think i can skip over these for now
```

Hey , can someone help me with this bug? I am reworking the conflicting notation with emojis https://github.com/meta-introspector/UniMath/pull/10

Ok, now I am working directly with ltac2 in the hope to later bring in unimath without need for changng any code. I have gotten coq to crash again.

Last updated: Jul 23 2024 at 20:01 UTC