Stream: MetaCoq

Topic: MetaCoq Tutorial at POPL


view this post on Zulip Matthieu Sozeau (Jan 13 2024 at 16:45):

This stream is dedicated to the tutorial on Sunday Jan 15th at POPL.

https://github.com/MetaCoq/metacoq/wiki/MetaCoq-Tutorial-@-POPL%C2%A02024:-Meta%E2%80%90programming-and-proving-with-MetaCoq

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

isn't sunday the 14th not 15th?

view this post on Zulip Julio Di Egidio (Jan 14 2024 at 07:48):

Hi guys, I am worried I might not have the needed setup: with coq-lsp installed from Snap on Ubuntu, I have tried to compile one random file from the examples and it works, but coq via Snap supposedly is not enough?

(I also have a Win installation from opam with Cygwin, although that one I am not sure in which state it is.)

view this post on Zulip Yannick Forster (Jan 14 2024 at 07:49):

If you can compile files importing things from MetaCoq you should be fine

view this post on Zulip Mario Carneiro (Jan 14 2024 at 08:02):

I have metacoq itself checked out, but I don't know how to create a new project depending on metacoq. Is there some opam new or equivalent I should be using, or should I just copy and cannibalize some other coq project?

view this post on Zulip Julio Di Egidio (Jan 14 2024 at 08:05):

I have metacoq itself checked out, but I don't know how to create a new project depending on metacoq

I think that is going to be part of the tutorial.

On the other hand, I have just realized it's 9.00 London time... :)

view this post on Zulip Mario Carneiro (Jan 14 2024 at 08:08):

starts in ~1hr, and only 10 minutes are allocated to installation so I'm guessing it's best to figure things out before it starts

view this post on Zulip Mario Carneiro (Jan 14 2024 at 08:11):

currently I'm just testing things out by creating new files in metacoq itself, but possibly that isn't the preferred approach

view this post on Zulip Julio Di Egidio (Jan 14 2024 at 08:12):

It would be nice to have the 4 lines of Coq needed to check that everything is there. -- I couldn't find it, whence I have simply opened and tried to compile something from the examples...

view this post on Zulip Yannick Forster (Jan 14 2024 at 08:14):

If From MetaCoq Require Import All. works you should be good to go

view this post on Zulip Julio Di Egidio (Jan 14 2024 at 08:20):

Yannick Forster said:

If From MetaCoq Require Import All. works you should be good to go

Thanks Yannick.

That does not work for me (maybe needs a _CoqProject?), but this does:

Require Import MetaCoq.Template.All.

view this post on Zulip Mario Carneiro (Jan 14 2024 at 08:22):

same here (the first one was an ambiguous import)

view this post on Zulip Yannick Forster (Jan 14 2024 at 08:25):

Ah, oops. You're good!

view this post on Zulip Mario Carneiro (Jan 14 2024 at 09:05):

has the meeting started? the zoom link seems to be stuck at "waiting for host to start the meeting"

view this post on Zulip Matthieu Sozeau (Jan 14 2024 at 09:08):

It should work now

view this post on Zulip Yannick Zakowski (Jan 14 2024 at 10:18):

I won't be able to attend the second part in order to cheer for a student in another session: is there any chance to have already access to the exercises that will be covered by any chance?

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 10:19):

https://github.com/MetaCoq/tutorials/tree/main/popl24/exercises

view this post on Zulip Yannick Zakowski (Jan 14 2024 at 10:19):

Thanks Théo!

view this post on Zulip Mario Carneiro (Jan 14 2024 at 10:49):

remark on the exercises: there are no actually working examples in there. It would be helpful to have a working example followed by an example to be completed by the reader

view this post on Zulip Meven Lennon-Bertrand (Jan 14 2024 at 10:54):

I think the idea is to have some of these examples as live coding in a moment

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 10:55):

Yes, you're going to be guided for the exercises.

view this post on Zulip Meven Lennon-Bertrand (Jan 14 2024 at 10:55):

(And there is the deep identity lower down in the file + stuff in live_coding.v)

view this post on Zulip Julin Shaji (Jan 14 2024 at 11:09):

I got error in this line in the tutorial: From MetaCoq Require Import bytestring.
Any idea to fix it?

view this post on Zulip Matthieu Sozeau (Jan 14 2024 at 11:10):

What’s the error message?

view this post on Zulip Julin Shaji (Jan 14 2024 at 11:12):

This one:

Required library bytestring matches several files in path (found
/home/user/.opam/4.14.1/lib/coq/user-contrib/MetaCoq/Quotation/ToPCUIC/Utils/bytestring.vo,
/home/user/.opam/4.14.1/lib/coq/user-contrib/MetaCoq/Quotation/ToTemplate/Utils/bytestring.vo and
/home/user/.opam/4.14.1/lib/coq/user-contrib/MetaCoq/Utils/bytestring.vo).

Removing that single line made it go away though.

view this post on Zulip Julin Shaji (Jan 14 2024 at 11:12):

In live_coding.v file

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 11:12):

From MetaCoq.Utils Require Import bytestring maybe?

view this post on Zulip Julin Shaji (Jan 14 2024 at 11:13):

Yeah that made it work. Thanks!

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 11:13):

It failed because you installed more of MetaCoq and there was an ambiguity. But it's our fault.

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:34):

Does MetaCoq Run ignore the return value? Is there a way to print kername or global_reference?

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:35):

MetaCoq Run (tmLocate1 "Coq.Init.Datatypes.nat").

does nothing

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 11:36):

Ah right, you probably need to bind it with tmPrint.

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:38):

oh, I tried something like

MetaCoq Run (kn <- tmLocate1 "nat";; tmPrint ("result: " ++ toString kn)).

but I don't know what the name of the tostringish classes are

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:39):

oh wow, tmPrint has no typeclass assumptions at all

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 11:39):

Maybe you can also do two tmPrint in a row.

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:40):

oh I see, it's printing the expression itself rather than evaluating it

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:40):

ooh, anomaly spotted

MetaCoq Run (kn <- tmLocate1 "nat";; tmPrint (kn + 1)).

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 11:40):

Yes. You can use tmEval to evaluate.

view this post on Zulip Matthieu Sozeau (Jan 14 2024 at 11:49):

The anomaly is due to evars remaining in the term, but I'm surprised that (kn + 1) typechecks at all

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:50):

it doesn't, but it seems that this surfaces as some unresolved evar

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:51):

the error message with Check is

Unable to unify "TemplateMonad global_reference" with "?m nat" (cannot unify "global_reference" and
"nat").;

view this post on Zulip Mario Carneiro (Jan 14 2024 at 11:52):

Maybe this is reported as a non-fatal error?

view this post on Zulip Matthieu Sozeau (Jan 14 2024 at 11:53):

Yep, it gets lost because ?m is not resolved

view this post on Zulip Matthieu Sozeau (Jan 14 2024 at 11:54):

Usually we use Definition tac := .... MetaCoq Run tac which will give you a meaningful message.

view this post on Zulip Julin Shaji (Jan 14 2024 at 11:58):

Is Yannick saying something? The zoom is muted.

view this post on Zulip Matthieu Sozeau (Jan 14 2024 at 11:59):

MetaCoq Run (tmBind (tmLocate1 "nat") (fun kn => tmPrint (1 + kn))). also gives back a meaningful type error

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 11:59):

Julin Shaji said:

Is Yannick saying something? The zoom is muted.

Nope, now we just help people individually, including online. ;)

view this post on Zulip Julin Shaji (Jan 14 2024 at 12:02):

For getting list of axioms, we first got to look into the environment, right?
I suppose global_decl global_env is type of global env.

view this post on Zulip Julin Shaji (Jan 14 2024 at 12:02):

Is there a separate local env type as well?

view this post on Zulip Julin Shaji (Jan 14 2024 at 12:03):

Are there docs mentioning the types and their meanings somewhere?

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:04):

that was on the slides, were they posted?

view this post on Zulip Julin Shaji (Jan 14 2024 at 12:04):

Yeah I got the global_env thing from slides.

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 12:05):

Slides are there: https://github.com/MetaCoq/tutorials/tree/main/popl24

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 12:06):

(Tutorial is going till 12:30 so you can stick around.)

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 12:06):

Julin Shaji said:

For getting list of axioms, we first got to look into the environment, right?
I suppose +global_decl+ global_env is type of global env.

Yeah the idea is to use lookup_env when you reach a constant to see whether it has a body or not.

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 12:06):

The rest is just traversing the term and collecting names of constants referring to axioms.

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 12:07):

You also have lookup_constant that's made for constants.

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:10):

What is Cumulative Inductive?

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:12):

(I notice that without the Cumulative it seems to take forever to compile...)

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 12:12):

(To people who left early, we're happy to answer your questions on the Zulip anytime!)

view this post on Zulip Meven Lennon-Bertrand (Jan 14 2024 at 12:13):

It's when cumulativity works not just for Type@{i} but also at the level of inductive types. Like if you have a polymorphic List and some l : List@{i} A then you can also type-check it at List@{j} A given the right relation between i and j

view this post on Zulip Meven Lennon-Bertrand (Jan 14 2024 at 12:13):

And yes, like any universe-polymorphic thing in Coq it has the tendency to have bad performances

view this post on Zulip Matthieu Sozeau (Jan 14 2024 at 12:18):

In case of list the universe is irrelevant. But for, say, Group@{i} := { carrier : Type@{i}; … }, Group@{i} <= Group@{j} when i <= j (assuming i is used covariantly in the Group definition)

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:23):

Don't inductives automatically infer variance? (that's the BiFinite thing IIRC)

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:25):

How are kernames represented in metacoq? When I saw this type I was quite confused because it has two names and sometimes one is used and sometimes the other one is and neither one seems like the "main" one

view this post on Zulip Théo Winterhalter (Jan 14 2024 at 12:26):

If you use Cumulative then yes, but by default it's going to be ridig. list@{i} A is not going to be a subtype of list@{i+1} A.

view this post on Zulip Meven Lennon-Bertrand (Jan 14 2024 at 12:27):

Mario Carneiro said:

Don't inductives automatically infer variance? (that's the BiFinite thing IIRC)

BiFinite is not about this, it is about whether the inductive is an inductive (Finite), coinductive (CoFinite) or variant (non-inductive, BiFinite).

view this post on Zulip Meven Lennon-Bertrand (Jan 14 2024 at 12:28):

Mario Carneiro said:

How are kernames represented in metacoq? When I saw this type I was quite confused because it has two names and sometimes one is used and sometimes the other one is and neither one seems like the "main" one

I think you have a modpath which represents the path to the module where the definition is, then the name of the definition proper

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:29):

oh, I was thinking of kerpair

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:29):

which is the name of mutual inductives and constants in the coq kernel (not sure about the metacoq kernel)

view this post on Zulip Meven Lennon-Bertrand (Jan 14 2024 at 12:30):

Not sure what you mean, About kerpair. does not return anything to me?

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:31):

it must be a coq-only thing then

view this post on Zulip Meven Lennon-Bertrand (Jan 14 2024 at 12:32):

Maybe so?

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:32):

the difference has something to do with modules so I suppose that's part of it

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:32):

I think for regular definitions both names coincide

view this post on Zulip Mario Carneiro (Jan 14 2024 at 12:34):

yeah, it's just using the "canonical name"

      | Constr.Const (c,pu) ->
        let kn = Constant.canonical c in
        (Q.mkConst (Q.quote_kn kn) (Q.quote_univ_instance pu), add_constant kn acc)

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2024 at 12:36):

AFAIU Metacoq doesn't handle anything module-related, and kerpairs are precisely here to handle module aliasing, so it makes sense not to expose them to the user in metacoq.

view this post on Zulip Mario Carneiro (Jan 14 2024 at 13:11):

Is there a reference for how names work in the module system? Are declarations re-typechecked after module instantiation, or does coq assume this works without rechecking?

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2024 at 13:56):

The answer to your second question is no. As for the first one, not really.

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2024 at 14:01):

I think that Élie Soubiran's PhD manuscript gives some insight into the current implementation: https://hal.science/tel-00679201v1 but that's far from being a comprehensive reference

view this post on Zulip Mario Carneiro (Jan 14 2024 at 15:14):

Just for clarification: the "module system evolution" described in section 2.3 was never actually adopted, right? The issue in 2.3.2 seems to still be present in recent versions of Coq

view this post on Zulip Pierre-Marie Pédrot (Jan 14 2024 at 15:16):

Indeed, I don't think so. Functors in Coq are still not applicative as of today.

view this post on Zulip Paolo Giarrusso (Jan 15 2024 at 01:05):

I've run before into Jacek Chrza̧szcz's work on Coq modules, do you know if that's still relevant? As a user, it seemed to be

view this post on Zulip Paolo Giarrusso (Jan 15 2024 at 01:19):

Ah, that's cited in that thesis; and Coq doesn't seem to unify module types and modules either

view this post on Zulip Pierre-Marie Pédrot (Jan 15 2024 at 07:31):

Internally, it kind of does, and there are some implicit casts going on from the user point of view sometimes (e.g. you can include a module type). Note that the module vs module type separation is a different problem than the one I was referring to, which is the crazy handling of name aliasing inherited from the ML world when we have dependent types with computation in types around (see the famous "F-ing modules" about the applicative case for a clear model of what we want).

view this post on Zulip Bas Spitters (Jan 15 2024 at 09:11):

@Pierre-Marie Pédrot IIRC the modules in Coq were developed in that way precisely so one could extract to ML modules. So, it seems we may be stuck with that design, as long as we want to extract to ML modules, aren't we?

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 15:21):

@Bas Spitters This is both rather true and a really naive illusion. Most of the kernel complexity around modules is indeed due to the fact that extraction does its best effort to preserve the Coq module structure. At the same time, the Coq type system and the OCaml type system are completely orthogonal already without modules, so pretending to type extracted Coq programs with OCaml types is bound to end up in explosive failure (outside of a ridiculously small fragment). I am not even talking about the potential mishap arising from mistmatches between the two module type systems (and there are quite a few). To me, it seems thus quite bonkers to hardwire a design choice around a process known to be deeply flawed.

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 15:22):

Module extraction is not the only source of craziness in the kernel, though. The PhD I cited above spills the beans: the current module system of Coq has been designed to not break backwards compatibility with Ltac code.

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 15:23):

This crazy aliasing mechanism is only there to please the tactic layer, so that all the previous code works up to aliasing without having to pass an explicit equivalence state between names.

view this post on Zulip Karl Palmskog (Jan 16 2024 at 15:23):

does coq-malfunction address any of the module-related extraction issues?

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 15:25):

Yes and no. It changes the spec of extraction by not trying to pretend to keep OCaml types around.

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 15:25):

But AFAIK modules are a no-go so far.

view this post on Zulip Matthieu Sozeau (Jan 16 2024 at 15:27):

coq-malfunction is based on the MetaCoq erasure which goes ‘though’ modules. I think it’s more or less doing the same thing as if we were defunctorizing everything and ignoring types entirely. E.g, module types would have no representation there.

view this post on Zulip Karl Palmskog (Jan 16 2024 at 15:28):

but then that would seem to get around PMP's complaints about the Coq/OCaml module systems being orthogonal?

view this post on Zulip Karl Palmskog (Jan 16 2024 at 15:30):

for many applications, I can see defunctorization working out fine for the Coq code one wants to verify and run, as long as one could establish a nice interface to it at OCaml level (or below)

view this post on Zulip Matthieu Sozeau (Jan 16 2024 at 15:58):

And there is currently no way to extract a functor, only its instances

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 16:07):

@Karl Palmskog indeed, as long as you ditch types you should be fine. A module in OCaml is just a record at runtime.

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 16:07):

My rant is not about extraction in the abstract, but the amount of crap we stuffed in the Coq kernel to support something that is unsound by construction.

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

well, then let's hope we can get proper support for malfunction-based extraction projects into 8.20, and that existing projects might switch to it over time

view this post on Zulip Matthieu Sozeau (Jan 16 2024 at 16:11):

Actually this makes me think, couldn’t we extend the erasure to functors, just reusing the lambda abstraction of lambda-box ? I don’t know what is the Ocaml/malfunction representation for those.

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 16:11):

AFAIU OCaml functors seen as first-class values are regular closures

view this post on Zulip Matthieu Sozeau (Jan 16 2024 at 16:12):

Ok, so that’s probably a yes

view this post on Zulip Pierre-Marie Pédrot (Jan 16 2024 at 16:12):

there is some magic to assign a position in a module to some name but I think this is done at compile-time

view this post on Zulip Matthieu Sozeau (Jan 16 2024 at 16:14):

Yeah, there must be some annotations somewhere to partially evaluate applied functor closures or give the right offsets

view this post on Zulip Matthieu Sozeau (Jan 16 2024 at 16:14):

I guess

view this post on Zulip JInhua Wu (Jan 18 2024 at 22:24):

Hi, I am new to the metacoq and gained a lot form this tutorial. I am working on a project and trying to use MetaCoq to derive some free theorems using parametricty. I notice that there are some todo in translations/param_binary.v. Is the parametricity in MetaCoq still in experiment?

view this post on Zulip Karl Palmskog (Jan 18 2024 at 22:45):

for parametricity, I'd take a close look at the following projects:

view this post on Zulip JInhua Wu (Jan 18 2024 at 22:57):

Thand you Karl! I will take a look at them.

view this post on Zulip Théo Winterhalter (Jan 19 2024 at 09:30):

I think the parametricity in MetaCoq was never finished indeed.

view this post on Zulip Basile Gros (Jan 22 2024 at 09:52):

Good morning,
I tried to execute the MetaCoq Check command given in the first presentation, but Coq raises a vernac error. Is there a PCUIC library that you need to import ?

view this post on Zulip Yannick Forster (Jan 22 2024 at 09:56):

You should be able to do

Require Import MetaCoq.Checker.Loader.
Definition foo := 2 * 2.

MetaCoq Check foo.

view this post on Zulip Yannick Forster (Jan 22 2024 at 09:57):

After installing coq-metacoq-checker

view this post on Zulip Théo Winterhalter (Jan 22 2024 at 09:57):

You can also use the verified checker with

Require Import MetaCoq.SafeChecker.Loader.
MetaCoq SafeCheck foo.

To get the safe checker you need to install it: opam install coq-metacoq-safechecker I think.

view this post on Zulip Yannick Forster (Jan 22 2024 at 10:00):

JInhua Wu said:

Hi, I am new to the metacoq and gained a lot form this tutorial. I am working on a project and trying to use MetaCoq to derive some free theorems using parametricty. I notice that there are some todo in translations/param_binary.v. Is the parametricity in MetaCoq still in experiment?

There's another incomplete but potentially better implementation of parametricity here: https://github.com/NeuralCoder3/metacoq/tree/unary-param/paramvar

view this post on Zulip Basile Gros (Jan 22 2024 at 10:27):

Théo Winterhalter said:

You can also use the verified checker with

Require Import MetaCoq.SafeChecker.Loader.
MetaCoq SafeCheck foo.

To get the safe checker you need to install it: opam install coq-metacoq-safechecker I think.

I have the package installed, but coq can't find the logical path when importing.

view this post on Zulip Basile Gros (Jan 22 2024 at 10:37):

Though I can import other SafeChecker files, like PCUICErrors.

view this post on Zulip Théo Winterhalter (Jan 22 2024 at 10:42):

That's odd, because they're both in the same folder: https://github.com/MetaCoq/metacoq/tree/coq-8.18/safechecker/theories

view this post on Zulip Basile Gros (Jan 22 2024 at 10:45):

I just checked, loader is the only file from that folder that I cannot import. Is it because it is not in the _CoqProject file in the parent directory ?

view this post on Zulip Théo Winterhalter (Jan 22 2024 at 10:48):

Right probably, I don't know why it was removed, maybe @Yannick Forster knows?

view this post on Zulip Paolo Giarrusso (Jan 22 2024 at 10:58):

(deleted)

view this post on Zulip Yannick Forster (Jan 22 2024 at 11:45):

Ah oops, that explains why I could only do it on older switches

view this post on Zulip Yannick Forster (Jan 22 2024 at 11:46):

Try coq-metacoq-safechecker-plugin

view this post on Zulip Yannick Forster (Jan 22 2024 at 11:46):

I think all of the plugins were moved to separate opam packages a while ago

view this post on Zulip Basile Gros (Jan 22 2024 at 12:20):

Yannick Forster said:

Try coq-metacoq-safechecker-plugin

Opam tells me it's already installed.

view this post on Zulip Yannick Forster (Jan 22 2024 at 12:28):

Really sorry for this, we'll have to debug a bit

view this post on Zulip Yannick Forster (Jan 22 2024 at 12:28):

Can you try ls ~/.opam/NAMEOFYOURSWITCH/lib/coq/user-contrib/MetaCoq/SafeCheckerPlugin

view this post on Zulip Basile Gros (Jan 22 2024 at 12:32):

Basile Gros said:

Yannick Forster said:

Try coq-metacoq-safechecker-plugin

Opam tells me it's already installed.

I can load MetaCoq.SafeCheckerPlugin.Loader, and MetaCoq SafeCheck works in that case. Sorry for the confusion.

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

So the dead Loader.v should be removed? It seems that is what caused confusion

view this post on Zulip Yannick Forster (Jan 22 2024 at 13:22):

No, I don't think anything needs to be removed

view this post on Zulip Paolo Giarrusso (Jan 22 2024 at 13:23):

There are two Loader.v files, but one won't be compiled

view this post on Zulip Paolo Giarrusso (Jan 22 2024 at 13:23):

Good: https://github.com/MetaCoq/metacoq/blob/coq-8.18/safechecker-plugin/theories/Loader.v
Bad: https://github.com/MetaCoq/metacoq/blob/coq-8.18/safechecker/theories/Loader.v

view this post on Zulip Yannick Forster (Jan 22 2024 at 13:24):

Oh right, it's even more confusing than I thought

view this post on Zulip Yannick Forster (Jan 22 2024 at 13:24):

Yes, I agree, the second one should go

view this post on Zulip Paolo Giarrusso (Jan 22 2024 at 13:26):

Aside: Honestly, I think _CoqProject files should just never list source files: just use wildcards (with find) when calling coq_makefile, which is the semantics you get in dune. Then this incorrect refactoring would be impossibile.

view this post on Zulip Yannick Forster (Jan 22 2024 at 13:26):

I definitely agree. The MetaCoq build process is quite complicated and has organically grown though, refactoring it to something sensible would be a major project

view this post on Zulip Basile Gros (Jan 22 2024 at 14:58):

I have an other question.

I found that in 8.18, MetaCoq Run sends an anomaly if you Run a piece of code that is not typed correctly, and that the Coq typechecker rejects.

If 8.16, it only sends an error, not an anomaly.

Should I submit a bug report ?

I have a small iexample file attached :
Exemple_minimal.v

view this post on Zulip Yannick Forster (Jan 22 2024 at 14:59):

Thank you! Submitting an issue in the MetaCoq repo would be great

view this post on Zulip Basile Gros (Jan 22 2024 at 15:28):

Done.

view this post on Zulip Julin Shaji (Feb 10 2024 at 06:03):

Not a metacoq question, but in these slides:
https://github.com/MetaCoq/tutorials/blob/main/popl24/The_MetaCoq_Formalisations.pdf

which I guess is made with beamer, lines of code are stepped through with highlighting.
In slides 4, 5 and 6.

I had been looking for a way to do that but couldn't find one with my
level of latex proficiency.

Could you tell me how this effect can be achieved? Is that code
snippet a minted environment?

We don't have to duplicate the entire snippet again and again with
different line highlighted, do we?

view this post on Zulip Théo Winterhalter (Feb 10 2024 at 22:06):

This is a question for @Meven Lennon-Bertrand.

view this post on Zulip Meven Lennon-Bertrand (Feb 19 2024 at 14:30):

Yes, this is minted + manual copy-pasting of the entire snippet, sadly… I couldn't find any smarter way to do it

view this post on Zulip Meven Lennon-Bertrand (Feb 19 2024 at 14:31):

I guess a better possibility would be to have code in an external file and use \inputminted + line highlighting to save the copy-pasting.

view this post on Zulip Julin Shaji (Feb 19 2024 at 16:53):

Meven Lennon-Bertrand said:

Yes, this is minted + manual copy-pasting of the entire snippet, sadly… I couldn't find any smarter way to do it

Ah.. I thought a better way discovered..

view this post on Zulip Julin Shaji (Feb 19 2024 at 16:54):

Meven Lennon-Bertrand said:

I guess a better possibility would be to have code in an external file and use \inputminted + line highlighting to save the copy-pasting.

That sounds better than copy pasting all over the place. Thanks!


Last updated: Jul 23 2024 at 20:01 UTC