Stream: MetaCoq

Topic: Metacoq notations


view this post on Zulip Mike DuPont (Jan 16 2024 at 13:18):

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

view this post on Zulip Notification Bot (Jan 16 2024 at 13:24):

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

view this post on Zulip Karl Palmskog (Jan 16 2024 at 13:26):

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

view this post on Zulip Mike DuPont (Jan 16 2024 at 14:10):

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.

view this post on Zulip Mike DuPont (Jan 16 2024 at 14:15):

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

view this post on Zulip Mike DuPont (Jan 16 2024 at 14:32):

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

view this post on Zulip Mike DuPont (Jan 16 2024 at 15:13):

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

view this post on Zulip Mike DuPont (Jan 16 2024 at 15:56):

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.

view this post on Zulip Mike DuPont (Jan 16 2024 at 17:16):

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

view this post on Zulip Mike DuPont (Jan 16 2024 at 20:43):

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

view this post on Zulip Karl Palmskog (Jan 16 2024 at 20:59):

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

view this post on Zulip Paolo Giarrusso (Jan 16 2024 at 22:06):

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.

view this post on Zulip Karl Palmskog (Jan 16 2024 at 22:07):

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.

view this post on Zulip Karl Palmskog (Jan 16 2024 at 22:08):

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.

view this post on Zulip Paolo Giarrusso (Jan 16 2024 at 22:11):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 13:08):

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 :)

view this post on Zulip Mike DuPont (Jan 26 2024 at 20:18):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 20:51):

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. :/

view this post on Zulip Gaëtan Gilbert (Jan 26 2024 at 20:53):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 20:54):

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

view this post on Zulip Karl Palmskog (Jan 26 2024 at 20:54):

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)

view this post on Zulip Karl Palmskog (Jan 26 2024 at 20:55):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 20:56):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 20:56):

yes i was thinking about going to lsp or semgrep next

view this post on Zulip Karl Palmskog (Jan 26 2024 at 20:56):

you need multiple -R clauses

view this post on Zulip Mike DuPont (Jan 26 2024 at 20:57):

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2024 at 20:57):

they say that type in type is not enabled yet

no, unimath uses type-in-type globally

view this post on Zulip Mike DuPont (Jan 26 2024 at 20:57):

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

view this post on Zulip Karl Palmskog (Jan 26 2024 at 20:59):

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)

view this post on Zulip Mike DuPont (Jan 26 2024 at 21:00):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 21:01):

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

view this post on Zulip Karl Palmskog (Jan 26 2024 at 21:01):

for example, here is a PR adding support for impredicative-set: https://github.com/ejgallego/coq-serapi/commit/4fb4e6b2d032b6d2ee09984de0876a6be636a21a

view this post on Zulip Mike DuPont (Jan 26 2024 at 21:02):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 21:03):

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

view this post on Zulip Gaëtan Gilbert (Jan 26 2024 at 21:09):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 21:14):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 21:19):

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

view this post on Zulip Mike DuPont (Jan 26 2024 at 21:52):

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".```

view this post on Zulip Mike DuPont (Jan 26 2024 at 21:54):

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

view this post on Zulip Mike DuPont (Jan 27 2024 at 17:53):

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

view this post on Zulip Mike DuPont (Jan 31 2024 at 21:33):

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: Oct 13 2024 at 01:02 UTC