Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Revise closed term extraction #467

Open
Kha opened this issue May 15, 2021 · 1 comment
Open

Revise closed term extraction #467

Kha opened this issue May 15, 2021 · 1 comment
Labels
depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it enhancement New feature or request
Projects
Compiler refactoring

Comments

@Kha
Copy link
Member

Kha commented May 15, 2021

Currently closed terms are evaluated eagerly at startup, which creates unnecessary overhead and linking dependencies. We want to move to bounded normalization at compile time, emit static code as in #122 if normalization succeeded, and otherwise create static code for a thunk to implement lazy once-only evaluation.
@Kha
Copy link
Member Author

Kha commented May 26, 2021

Note: we should double-check to not compile-time evaluate any values dependent on getIsWindows and similar functions.

@Kha Kha mentioned this issue Jun 22, 2021
Closed
1 task
leodemoura added a commit that referenced this issue Jun 29, 2021
@leodemoura
fix: disable panic messages during initialization
2018dc0 
This is a temporary workaround until we implement #467.
Fixes #534
@Kha Kha mentioned this issue Dec 22, 2021
Merged
@leodemoura leodemoura added the enhancement New feature or request label Jun 1, 2022
@leodemoura leodemoura added the depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it label Aug 4, 2022
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
@semorrison
feat: port Algebra/CovariantAndContravariant (leanprover#467)
d0b0a73 
These are mostly instances required so that lemmas needed for linarith actually fire in the presence of `LinearOrderedCommRing`.

- [x] depends on leanprover#457 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
@semorrison
feat: partial port of Algebra/Order/ (leanprover#470)
a26dc82 
These aren't complete ports, mostly just the typeclass definition parts of
* `Algebra.Order.Monoid`
* `Algebra.Order.Group`
* `Algebra.Order.Ring`

Creating these typeclasses with sorried instances for use with `linarith` was barely easier than porting the instances too.

- [x] depends on leanprover#467 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@Kha Kha mentioned this issue Jul 23, 2023
Closed
1 task
@Kha Kha mentioned this issue Feb 7, 2024
Open
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
depends on new code generator We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it enhancement New feature or request
Projects
Compiler refactoring
To Do
Milestone
No milestone
Development

No branches or pull requests
2 participants
@Kha @leodemoura