mit-plv / rewriter Goto Github PK

The Coq team released Coq 8.19.0 on January 24th, 2024.
The corresponding Coq Platform release 2024.01 should be released before April 30th, 2024.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.19.0.

Coq Platform CI is currently testing opam package coq-rewriter.0.0.10
from official repository https://coq.inria.fr/opam/released/packages/coq-rewriter/coq-rewriter.0.0.10/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2024.01, please inform us as soon as possible and before March 31st, 2024!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.19~2024.01+beta1 which already supports Coq version 8.19.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#405

I don't think the rewriter is suitable for wider adoption. It's very, very, very much a research prototype, and I don't see it becoming not a research prototype without going through a complete rewriting. Almost all of it is either a pile of hacks or proofs which are made very painful by inline CPS and dependent types. It's going to be hard to maintain, too, in it's current form. I think the ideas are good, but the implementation is just good enough to work for fiat-crypto. (Recall that the prior state-of-the-art was writing the pattern matches on PHOASTs by hand.) An incomplete list of things that I think need to be rewritten from scratch:

1. The code for creating the rewriter is currently a messy mixture of a bit of OCaml plugin code for adding inductives and setting the strategy of things (this should be replaced by something like coq-elpi or MetaCoq), and a large amount of exremely hacky Ltac code that should be replaced by something more maintainable
2. Generation of the various necessary properties of the syntax languages should be streamlined and made more efficient, so that we incur less overhead when creating the language in the first place.
3. The code for reducing the rewriter early is currently a mess, because it was developed organically. It should be rewritten with an eye on what can be unfolded early and what needs to remain folded from the very start, possibly with some sort of type-driven separation of them. (There might be interesting research to do here.)
4. The proofs of the rewriter are not really maintainable, and are severely complicated by the use of CPS + dependent types. I think the way to go moving forward is to separate out two implementations of the rewriter, to be kept in sync: one that is CPS'd and fit for early reduction, and one that is not CPS'd and is clean to prove things about, but which ultimately can be proven equal to the CPS'd one.
5. Proving the side-conditions of reifying rewrite rules is currently a mess, because the rewriter was initially written without any intent to reify the rewrite rules, and instead was intended to have them proven by hand. The rewrite of the rewriter should follow the standard proof-by-reflection methodology, where the reification can be proven equal to the denotation via reflexivity, and then the only side-condition needed on the reified AST is a well-formedness predicate. (Then we can simply ask for a proof of the denotation of the reified rewrite rule.) All further transformations should happen reflectively rather than during the reification process, and the rewriter should be built around the presumption that this is where rules will be coming from. (This will incidentally simplify some of the dependent types, which were present only to make hand-writing rewrite rules nicer.)
6. There are a number of restrictions that should be lifted, the chief among them being the requirement that matching is linear on non-constants. (@achlipala, does there exist somewhere a treatment of PHOAS transformations which are allowed to query equality of variable nodes? The only way I can think of to do this is to instantiate var with symbol * outvar where I have a splittable infinite stream of symbols available and symbol has decidable equality, manually generating new symbols at each lambda node, and maintaining proof state about equality of outvars matching equality of symbols. It seems like there's a lot of overhead here, and I'm wondering if this can actually be done nicely.)
7. The code should be set up from the get-go to support generalization to arbitrary container types (I believe the main blocker for this, theoretically-speaking, is knowing how to thread the let-binding monad with arbitrary container-eliminator types).
8. The fact that pattern matching compilation naturally operates on raw syntax while NbE naturally operates on intrinsically-typed syntax is an ugly wart that I'm not sure how to fix. The current rewriter code glues them together with ugly code and painful proofs, but I'd like to see an elegant treatment of fusing pattern-matching compilation with NbE. (This would require new research. But even without this, in a rewrite of the rewriter, the glue should be accounted for so that its impact can be localized.)

Originally posted by @JasonGross in mit-plv/fiat-crypto#833 (comment)

@JasonGross : I have an issue with the Coq Platform release for Coq 8.16.1: the coq-rewrite opam package does not build if the default shell is zsh rather than bash (zsh is the default since a few years on macOS). This is because zsh does not have a realpath command (it has other ways to achieve the same, but not compatible). The issue is here:

The Coq team released Coq 8.17+rc1 on December 29th, 2022 and plans to release Coq 8.17.0 around March 7th, 2023.
The corresponding Coq Platform release 2023.03 should be released before April 14th, 2023.
It can be delayed in case of difficulties until June 30, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.17+rc1.

Coq Platform CI is currently testing opam package coq-rewriter.0.0.6
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-rewriter/coq-rewriter.0.0.6/opam. Please note that version 0.0.7 does not compile on MacOS cause of stack size limitations.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.03, please inform us as soon as possible and before March 21st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.17~2023.03+preview1 which already supports Coq version 8.17+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#335

Of the time spent in the new rewrite rule reification, 82.7% is spent in replace_type_try_transport (236.006s max for a single call), which is basically "match context[@type.try_transport ?base_type ?try_make_transport_base_type_cps ?p ?t ?t], replace with p t" in a loop.

I have asked about speeding this up on Zulip, but at this point I'm inclined to run another timing diff after #142 and then eat the ~2--3 minute slowdown.

(I'm also out of debugging time, @andres-erbsen if you want to debug, consider applying the patch

diff --git a/src/Rewriter/Passes/NBE.v b/src/Rewriter/Passes/NBE.v
index 429a6125f..784248943 100644
--- a/src/Rewriter/Passes/NBE.v
+++ b/src/Rewriter/Passes/NBE.v
@@ -16,8 +16,14 @@ Module Compilers.

   Module Import RewriteRules.
     Section __.
-      Definition VerifiedRewriterNBE : VerifiedRewriter_with_args true false true nbe_rewrite_rules_proofs.
+      Set Ltac Profiling.
+      Set Printing Depth 1000000.
+      Ltac2 Set Rewriter.Language.PreCommon.Pre.reify_profile_cbn := Init.true.
+      Ltac2 Set Reify.should_debug_profile := fun () => Init.true.
+      Definition VerifiedRewriterNBE : VerifiedRewriter_with_args false false true nbe_rewrite_rules_proofs.
       Proof using All. make_rewriter. Defined.
+      Redirect "profile" Show Ltac Profile.
+      Redirect "profile0" Show Ltac Profile CutOff 0.

       Definition default_opts := Eval hnf in @default_opts VerifiedRewriterNBE.
       Let optsT := Eval hnf in optsT VerifiedRewriterNBE.
diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v
index 08d572064..1c4d81e04 100644
--- a/src/Rewriter/Rules.v
+++ b/src/Rewriter/Rules.v
@@ -51,7 +51,7 @@ Definition nbe_rewrite_rulesT : list (bool * Prop)
       myflatten
         [mymap
            dont_do_again
-           [(forall A B x y, @fst A B (x, y) = x)
+           [(*(forall A B x y, @fst A B (x, y) = x)
             ; (forall A B x y, @snd A B (x, y) = y)
             ; (forall P t f, @Thunked.bool_rect P t f true = t tt)
             ; (forall P t f, @Thunked.bool_rect P t f false = f tt)
@@ -183,7 +183,7 @@ Definition nbe_rewrite_rulesT : list (bool * Prop)
                             end)
                         ('n)
                         xs)
-              ; typeof! @unfold1_nat_rect_fbb_b
+              ; *)typeof! @unfold1_nat_rect_fbb_b
               ; typeof! @unfold1_nat_rect_fbb_b_b
               ; typeof! @unfold1_list_rect_fbb_b
               ; typeof! @unfold1_list_rect_fbb_b_b

You might also want to throw a Set Printing Implicit. or Set Printing All.. If you do want to debug this, let me know if there's any other information that would be useful to expose debugging-wise. And Ltac2 Set Reify.should_debug_fine_grained := fun () => Init.true. should give access to the argument to and return from replace_type_try_transport, though it'll give a bunch of other stuff as well.)

Originally posted by @JasonGross in mit-plv/fiat-crypto#1778 (comment)

The Coq team released Coq 8.18.0 on September 7th, 2023.
The corresponding Coq Platform release 2023.10 should be released before November 30th, 2023.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.18.0.

Coq Platform CI is currently testing opam package coq-rewriter.0.0.9
from official repository https://coq.inria.fr/opam/released/packages/coq-rewriter/coq-rewriter.0.0.9/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2023.10, please inform us as soon as possible and before October 31st, 2023!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.18+beta1 which already supports Coq version 8.18.0 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#372

The file https://github.com/mit-plv/rewriter/blob/master/src/Rewriter/Demo.v should be fleshed out and completed. Perhaps ideally in time for the POPL submission.

We should not rely Makefile.coq for the clean target unless we forcibly remake it or something, to avoid errors involving the move from .ml4 to .mlg

Currently, we cannot handle rewrite rules such as

forall x, '(S x) = pred '(S (S x))

because we end up generating a pattern like forall x1 x2, x1 =? S x && x2 =? S (S x) -> 'x1 = pred 'x2, and the reification machinery does not know how to invert these equations to eliminate x:

Presumably we could write some sort of custom inversion machinery to handle these constructors? And/or we could emit better error messages than just

Error:
Uncaught Ltac2 exception:
RewriteRules.Reify.Cannot_eliminate_functional_dependencies
  (message:((fun u2 : Z =>
             existT
               (RewriteRules.Compile.rewrite_ruleTP
                  IdentifiersGENERATED.Compilers.pattern.ident.arg_types_unfolded)
               {|
                 pattern.type_of_anypattern :=
                   type.base
                     (pattern.base.type.type_base Compilers.Z *
                      pattern.base.type.type_base Compilers.Z)%pbtype;
                 pattern.pattern_of_anypattern :=
                   #Compilers.pattern_ident_Z_cast2 @
                   (#(Compilers.pattern_ident_pair
                        (pattern.base.type.type_base Compilers.zrange)
                        (pattern.base.type.type_base Compilers.zrange)) @
                    #(Compilers.pattern_ident_Literal Compilers.zrange) @
                    #(Compilers.pattern_ident_Literal Compilers.zrange)) @
                   (#Compilers.pattern_ident_Z_mul_split @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)) @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)) @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)))
               |}
               {|
                 RewriteRules.Compile.rew_should_do_again := true;
                 RewriteRules.Compile.rew_with_opt := true;
                 RewriteRules.Compile.rew_under_lets := true;
                 RewriteRules.Compile.rew_replacement :=
                   fun (t t0 : ZRange.zrange)
                     (x0 x1
                      x2 : API.expr
                             (type.base (base.type.type_base Compilers.Z)))
                   =>
                   if
                    ((0 <=? 2 ^ bitwidth - 1)%Z && (0 <=? u1)%Z &&
                     (0 <=? u2)%Z &&
                     Definitions.Z.divideb (u1 + 1) (2 ^ bitwidth - 1 + 1) &&
                     Definitions.Z.divideb (u2 + 1) (2 ^ bitwidth - 1 + 1) &&
                     (negb (u1 =? 2 ^ bitwidth - 1)%Z
                      || negb (u2 =? 2 ^ bitwidth - 1)%Z) &&
                     ZRange.zrange_beq t
                       {| ZRange.lower := 0; ZRange.upper := u1 |} &&
                     ZRange.zrange_beq t0
                       {| ZRange.lower := 0; ZRange.upper := u2 |})%bool
                   then
                    Some
                      (RewriteRules.Reify.expr_value_to_rewrite_rule_replacement
                         (@RewriteRules.Compile.reflect_ident_iota
                            Compilers.base
                            IdentifiersBasicGENERATED.Compilers.ident
                            Compilers.base_interp Compilers.baseHasNat
                            Compilers.buildIdent Compilers.buildEagerIdent
                            Compilers.toRestrictedIdent
                            Compilers.toFromRestrictedIdent
                            Compilers.invertIdent Compilers.baseHasNatCorrect
                            Compilers.try_make_base_transport_cps var) true
                         (#Compilers.ident_Z_cast2 @
                          (###{| ZRange.lower := 0; ZRange.upper := u1 |},
                           ###{| ZRange.lower := 0; ZRange.upper := u2 |}) @
                          (#Compilers.ident_Z_cast2 @
                           (###{|
                                 ZRange.lower := 0;
                                 ZRange.upper := 2 ^ bitwidth - 1
                               |},
                            ###{|
                                 ZRange.lower := 0;
                                 ZRange.upper := 2 ^ bitwidth - 1
                               |}) @
                           (#Compilers.ident_Z_mul_split @ $$x0 @ $$x1 @ $$x2))))
                   else None
               |})))

I should really update the master job to pull from the latest git version / use opam, so I don't need to wait for Launchpad to rebuild and publish the master package before the CI can pass...

Originally posted by @JasonGross in #16 (comment)

I just tried to compile version 0.0.7 on an ARM / Apple silicon Mac. the maximum stack size one can specify on macOS is 64MB. This is sufficient to compile version 0.0.6, but it is not sufficient for 0.0.7.

It's quite painful to figure out why rewriter rules aren't matching. It should be possible, using a combination of reduction-effects for cbv (alas, no support for native_compute / vm_compute, yet; see coq-community/reduction-effects#8) and using extraction directives for OCaml/Haskell, to insert debug print calls in the main loop of the rewriter, to thread through and print out some sort of debugging information, with minimal overhead when we're not printing debug info.