Pierre-Marie Pédrot comments

Results 403 comments of


                                            Pierre-Marie Pédrot

[Experiment] Hack a global fixpoint expansion in conversion.

Now with refolding on lazy reduction only: @coqbot bench

[Experiment] Hack a global fixpoint expansion in conversion.

There are some huge variations in the per-line diff, but overall this looks like a neutral change.

Remove the Lforce node from the generic lambda AST.

I'll let the CI finish before fixing this, just to check whether we actually test anything about native compilation in there.

Remove the Lforce node from the generic lambda AST.

Should I seize the opportunity of this PR to integrate the proposed fixes in the discussion?

Remove the Lforce node from the generic lambda AST.

This tiny cleanup PR has uncovered to much broken stuff, calling for psychological / code help.

Remove the Lforce node from the generic lambda AST.

@coqbot run full ci

Remove the Lforce node from the generic lambda AST.

This should be ready. I haven't touched the semantics of laziness for array nodes since we probably need to decide for a more robust principle, but at least the cast...

Remove the Lforce node from the generic lambda AST.

This needs an assignee. @silene ?

Remove the Lforce node from the generic lambda AST.

Fixed.

Remove the Lforce node from the generic lambda AST.

@coqbot run full ci