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