Bas Spitters (Jun 16 2020 at 09:22): Bas Spitters (Jun 16 2020 at 09:22):What's the status of certicoq? The website does not give much information
https://www.cs.princeton.edu/~appel/certicoq/
Karl Palmskog (Jun 16 2020 at 09:24):would be interested in this as well, I believe many subprojects of CertiCoq like garbage collection would be super useful in their own right
Matthieu Sozeau (Jun 16 2020 at 09:34):We finally have a Coq 8.11 version, I hope a beta version can be released this month
Karl Palmskog (Jun 16 2020 at 09:40):@Matthieu Sozeau how does the packaging/reuse situation look? can one set up workflow for just hooking in to pre-installed CertiCoq into some extraction-based project and get something executable without extensive engineering?
Karl Palmskog (Jun 16 2020 at 09:41):(in e.g., Oeuf, there was quite a lot of laying-on-hands like creating a C shim, just wondering how it will compare)
Matthieu Sozeau (Jun 16 2020 at 09:44):There is some support already to generate C shims, but AFAIK you currently still have to compile and link the runtime by hand. We'll have that documented by the release for sure :)
Danil Annenkov (Jun 16 2020 at 14:23):L2 looks like CIC_box (somewhat), so is there any relation between the certified erasure in MetaCoq and one of the CertiCoq passes (maybe L2)?
Matthieu Sozeau (Jun 16 2020 at 20:19):Yes, they're linked CIC_box goes to L2.
Danil Annenkov (Jun 16 2020 at 20:23):Ah, great, thanks!
I think I asked this already, but anyway. Is there an optimisation in CertiCoq that removes redundant boxes? We @Jakob Botsch Nielsen @Bas Spitters are currently working on such a transformation.
Bas Spitters (Jun 18 2020 at 20:06):@Matthieu Sozeau to amplify what Danil is saying. It would seem that deboxing could also be a relevant optimization for certicoq.
Does that seem correct?
Matthieu Sozeau (Jun 19 2020 at 09:36):In CertiCoq there is no specific phase to remove boxes, but we expect the "shrink-reduction" phase to remove most of them. There is also a phase that removes parameters of constructors (after eta-expanding them). I think having a deboxing phase early in the pipeline (e.g. just after erasure) could help as well.
Bas Spitters (Jun 19 2020 at 09:48):We need to remove the boxes to extract to typed code, but it seems like it would be natural to aim to integrate this into the main certicoq pipeline.
Jakob Botsch Nielsen (Jun 26 2020 at 10:58):Matthieu Sozeau said:
In CertiCoq there is no specific phase to remove boxes, but we expect the "shrink-reduction" phase to remove most of them. There is also a phase that removes parameters of constructors (after eta-expanding them). I think having a deboxing phase early in the pipeline (e.g. just after erasure) could help as well.
Is this the stuff in L2k_noCnstrParams? As far as I can see there is no correctness proof of it, or am I missing something?
Matthieu Sozeau (Jun 29 2020 at 16:29):Yes, there used to be a proof of it but it's commented for now due to changes in the earlier languages (IIRCC)
Jakob Botsch Nielsen (Jun 30 2020 at 08:38):I'm not sure that I understand the code totally, but as far as I can tell that phase removes parameters and also simultaneously does eta expansion if the constructor is not applied to enough parameters (in the strip function). Then the commented correctness proof is saying that if t wcbv evaluates to p, then strip t will wcbv evaluate to strip p. But I don't think this holds in general for higher order values.
For example, say that foo is a constructor with two parameters. Then:
let x := foo 0 in fun y => x 1
evaluates to
fun y => foo 0 1
on its own. Stripping this results in fun y => foo.
If we strip before evaluation we transform
let x := foo 0 in fun y => x 1
to
let x := fun v => foo in fun y => x 1
and then this evaluates to
fun y => (fun v => foo) 1
which is not reduced further.
Matthieu Sozeau (Jun 30 2020 at 09:31):I agree, eta-expansion gives you only beta equivalent terms in the end.
Jakob Botsch Nielsen (Jun 30 2020 at 11:08):Aha, but just beta should be enough? No fixpoints/match evaluation should be necessary?
Bas Spitters (Jul 02 2020 at 08:17):About (certified) extraction to typed languages. Pierre Letouzey asks here whether SML has Obj.magic. The lack of answer makes me think it doesn't.
https://coq-club.inria.narkive.com/TVMVPzck/coq-sml-and-ada
Last updated: Feb 06 2023 at 06:29 UTC