Stream: CUDW 2020

Topic: The scary stuff thread [you've been warned]

Emilio Jesús Gallego Arias (Dec 01 2020 at 15:03):

@Pierre-Marie Pédrot @Enrico Tassi , I think @Gaëtan Gilbert has a good point in that refine is actually doing stuff that it has no business to do. In fact confirm that if we remove the push_private_partsfrom refine.ml , Coq compiles, and the test-suite passes. Also, my assert is never triggered.

This makes sense, as the functions creating side-effects are actually trying hard [to the best of their possibilites] to keep things in check when they create the side-eff, and IMHO that's the right approach. PR incoming

Pierre-Marie Pédrot (Dec 01 2020 at 15:06):

Yes but no.

Pierre-Marie Pédrot (Dec 01 2020 at 15:06):

You need to wrap the non-tactic function so as to replay the side-effects outside of it.

Pierre-Marie Pédrot (Dec 01 2020 at 15:06):

That is, generic_refine shouldn't be handling the environment reset, I agree

Pierre-Marie Pédrot (Dec 01 2020 at 15:07):

but unfortunately, Refine.refine would be unsound w.r.t. that

Pierre-Marie Pédrot (Dec 01 2020 at 15:07):

because side-effects also appear in the evarmap

Gaëtan Gilbert (Dec 01 2020 at 15:07):

what non tactic function

Pierre-Marie Pédrot (Dec 01 2020 at 15:08):

the thunk from Refine.refine

Pierre-Marie Pédrot (Dec 01 2020 at 15:08):

val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic

Gaëtan Gilbert (Dec 01 2020 at 15:08):

you mean the

let lift c =
  Proofview.tclEVARMAP >>= fun sigma ->
  Proofview.V82.wrap_exceptions begin fun () ->
  let (sigma, c) = c sigma in
  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
  Proofview.tclUNIT c
  end

should do the side effect dance?

Pierre-Marie Pédrot (Dec 01 2020 at 15:08):

yes

Pierre-Marie Pédrot (Dec 01 2020 at 15:10):

We have way too many states in Coq.

Pierre-Marie Pédrot (Dec 01 2020 at 15:12):

ping @Emilio Jesús Gallego Arias

Emilio Jesús Gallego Arias (Dec 01 2020 at 15:29):

I agree, however we are not so far from taming it a bit; down to proof state and vernacular state

Cody Roux (Dec 01 2020 at 15:46):

How about when you rewrite everything in Rust?

Enrico Tassi (Dec 01 2020 at 15:46):

in metacoq

Cody Roux (Dec 01 2020 at 15:47):

So Lean 4 :)

Pierre-Marie Pédrot (Dec 01 2020 at 15:48):

@Cody Roux you're joking but I seriously plan on writing some critical parts in Rust.

Pierre-Marie Pédrot (Dec 01 2020 at 15:48):

Like, universes.

Pierre-Marie Pédrot (Dec 01 2020 at 15:49):

(Am waiting for a proper OCaml-Rust FFI though, there is ongoing work on that it seems.)

Cody Roux (Dec 01 2020 at 18:13):

Exciting!

Enrico Tassi (Dec 01 2020 at 18:19):

Time to drop dune and use cargo [trolling]

Paolo Giarrusso (Dec 01 2020 at 21:18):

or bazel?

Enrico Tassi (Dec 01 2020 at 21:27):

Sounds like the name of a dutch sandwich, but looks amazing (some pun intended) ;-)

Pierre-Marie Pédrot (Dec 01 2020 at 21:33):

@Cody Roux a PhD student at the MPI went pretty far on the implementation of a Coq checker in Rust by the way.

Pierre-Marie Pédrot (Dec 01 2020 at 21:33):

https://github.com/pythonesque/kravanenn

Pierre-Marie Pédrot (Dec 01 2020 at 21:34):

Hm, sorry, not the right repo.

Cody Roux (Dec 01 2020 at 21:35):

I was wondering about this based on Jason's defense and some comments from Talia Ringer: how would one implement the kernel if the only consideration was fast proof checking and proof engines?

Pierre-Marie Pédrot (Dec 01 2020 at 21:35):

Aha. That's the trick: proof checking and proof engine are pretty much at odds.

Cody Roux (Dec 01 2020 at 21:36):

How so?

Enrico Tassi (Dec 01 2020 at 21:36):

They are twins PMP! How can they be at odds?

Cody Roux (Dec 01 2020 at 21:36):

also: Should I create a new thread, or are we still in-bounds for "scary stuff"?

Pierre-Marie Pédrot (Dec 01 2020 at 21:36):

Evil twins, maybe.

Pierre-Marie Pédrot (Dec 01 2020 at 21:37):

But except if you want to duplicate the code, you need to optimize different things in the two cases.

Pierre-Marie Pédrot (Dec 01 2020 at 21:37):

Oh, that's definitely scary.

Pierre-Marie Pédrot (Dec 01 2020 at 21:37):

It's a bit late for Halloween, but maybe a Red Xmas is thematic.

Enrico Tassi (Dec 01 2020 at 21:37):

with my crazy logic programming glasses, the proof engine is the kernel plus a bunch of rules of evars. If one gets faster, how is it's extension getting slower?

Cody Roux (Dec 01 2020 at 21:38):

Jason mentioned that instantiating Evars was a notable performance issue. In my experience, trying to do partial evaluation using simpl is a non-starter. And then obviously a bunch of Coq libraries are crazy slow to compile for various reasons

Pierre-Marie Pédrot (Dec 01 2020 at 21:38):

I am afraid that if we speak efficiency, logic programming is already dismissed.

Pierre-Marie Pédrot (Dec 01 2020 at 21:38):

Being serious, mind you, not even trolling (well).

Cody Roux (Dec 01 2020 at 21:39):

How about the primitives for logic programing? Like Evar instantiation, or unification?

Enrico Tassi (Dec 01 2020 at 21:39):

In matita the engine was a copy-past of the kernel, where assert false for the Evar branch was actually doing something. No logic programming there.

Pierre-Marie Pédrot (Dec 01 2020 at 21:39):

Yes, simpl is a no-starter.

Pierre-Marie Pédrot (Dec 01 2020 at 21:39):

So, on the one hand you want efficient evars in the proof engine.

Cody Roux (Dec 01 2020 at 21:39):

But vm_compute can't make things opaque! We ended up adding axioms in places where things needed to not be unfolded...

Pierre-Marie Pédrot (Dec 01 2020 at 21:39):

The best you can do is probably some mutable in-place structure for that.

Cody Roux (Dec 01 2020 at 21:40):

Is that how it is in Coq? I missed Emilio's talk yesterday.

Pierre-Marie Pédrot (Dec 01 2020 at 21:40):

vm_compute could perfectly make things opaque, I have a series of PR on the subject.

Pierre-Marie Pédrot (Dec 01 2020 at 21:40):

No, Coq uses a pure structure that is essentially a heap.

Enrico Tassi (Dec 01 2020 at 21:41):

In the crazy world of logic programming, i.e. Elpi, using mutability + a trail for "evar" assignment was 10x faster than using a purely functional map.

Pierre-Marie Pédrot (Dec 01 2020 at 21:41):

Without GC, without fast access, with a terrible memory representation.

Cody Roux (Dec 01 2020 at 21:41):

how about "opaque, but inside this subterm, compute again"? (Speaking of scary stuff)

Pierre-Marie Pédrot (Dec 01 2020 at 21:41):

@Cody Roux this is starting to get spooky

Pierre-Marie Pédrot (Dec 01 2020 at 21:42):

@Enrico Tassi well, this is not directly related to logic programming.

Cody Roux (Dec 01 2020 at 21:42):

Basically we tried to implement this: https://arxiv.org/abs/1612.06668 using vanilla Coq reduction

Enrico Tassi (Dec 01 2020 at 21:42):

mutability + trail is what I see on "typewriter" papers about Prolog.

Pierre-Marie Pédrot (Dec 01 2020 at 21:43):

Maybe we don't call the same thing LP which is why we disagree on its potential efficiency. To me, the defining feature of LP is a baked-in non-deterministic semantics.

Cody Roux (Dec 01 2020 at 21:44):

In Lean 1, higher-order unification could backtrack. This was a disaster for usability, and Lean 2 just failed if there were remaining flex/flex problems...

Pierre-Marie Pédrot (Dec 01 2020 at 21:44):

Ah yeah, I've seen this paper already;

Cody Roux (Dec 01 2020 at 21:45):

Leo's idea for Evar contexts seemed clever though: just close all evars with lambdas...

Pierre-Marie Pédrot (Dec 01 2020 at 21:45):

As a side-effect (pardon the pun) LP uses unification + backtrack for pretty much everything and the little game is to put a lot of cuts everywhere in order to counter this nonsense

Enrico Tassi (Dec 01 2020 at 21:45):

@Pierre-Marie Pédrot Even in LP bactracking is not super useful. 10% of the times you use it, 90% you "turn it off!". Still many things are nice.

Last updated: Jun 11 2023 at 00:30 UTC