leanprover / lean4 Goto Github PK
View Code? Open in Web Editor NEWLean 4 programming language and theorem prover
Home Page: https://lean-lang.org
License: Apache License 2.0
Lean 4 programming language and theorem prover
Home Page: https://lean-lang.org
License: Apache License 2.0
We should support
DecidableEq
HasBeq
HasToString
Repr
Inhabited
When a module with capital letters is imported into another module, the name of the module is inconsistently rendered in the generated code, eventually leading to missing symbol errors in the linker.
Expected behavior:
Program should compile and print "hi!" when run.
Actual behavior:
Missing symbols in the linker:
$ ./build.sh
+ export LEAN_PATH=/usr/local/lib/lean/library:.
+ LEAN_PATH=/usr/local/lib/lean/library:.
+ lean --make camelCase.lean
+ lean --make lowercase.lean
+ lean -c camelCase.cpp camelCase.lean
+ lean -c lowercase.cpp lowercase.lean
+ leanc -o test lowercase.cpp camelCase.cpp
Undefined symbols for architecture x86_64:
"initialize_camelCase(lean::object*)", referenced from:
initialize_lowercase(lean::object*) in lowercase-9b5b9c.o
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Examining the generated camelCase.cpp
we can find the function initialize_camelcase
, where the module name appears to have been forced into lowercase.
Reproduces how often: [What percentage of the time does it reproduce?]
100% reproducable
$ lean --version
Lean (version 4.0.0, commit 52b86c3b4b7e, Release)
macOS 10.14.6
Maybe this is related to issues with filesystem case-sensitivity?
The error messages don't know how to synthesize placeholder
are displaying an incorrect context
after commit 7842036.
For example:
theorem foo (a b : nat) (h : a = b) : b = a :=
_
produces the error message
error: don't know how to synthesize placeholder
context:
⊢ ∀ (a b : ℕ), a = b → b = a
instead of
error: don't know how to synthesize placeholder
context:
a b : ℕ
h : a = b
⊢ b = a
Commit 7842036 avoids the use of delayed abstractions when creating bindings (lambda/pi/let). The idea is simple for every metavariable ?m
occurring in the body of the binder e
, revert all locals in ?m
that are being abstracted, and obtain ?m1
. Then, ?m
is replaced with ?m1 x_1 ... x_n
where x_1 ... x_n
are the reverted locals.
The body of the theorem is just a placeholder which is elaborated into ?m
. The local context of ?m
contains a
, b
and h
. Then, when we abstract a b h
, we obtain fun (a b : nat) (h : a = b), ?m_1 a b h
, and the assignment ?m := ?m_1 a b h
. Then, the method elaborator::ensure_no_unassigned_metavars
incorrectly produces an error message for ?m_1
which has an empty context.
@Kha This problem is quite annoying, but it is not worth fixing now since we will re-write the elaborator. In the new elaborator, we should use a different approach where we record the metavariable created for each placeholder _
. Then, during finalization, we check whether these placeholders have been assigned or not. If they have been assigned to metavariables applications such as ?m_1 a b h
, we just report the error for ?m
instead of ?m_1
.
$ LEAN_PATH=Init=wrong bin/lean scratch.lean
[2] 24627 segmentation fault (core dumped)
This is because
Line 102 in 2509b39
IO.Error
representation.
/cc @cipher1024
The new approach we use for compiling dependent pattern matching produces expressions that can be pretty-printed using the match ... with ...
. We generate a "matcher" auxiliary function for each match
-expression. The "matchers" have the following structure:
lean4/src/Lean/Meta/Match/Match.lean
Lines 726 to 734 in d33f7c7
lean4/src/Lean/Meta/Match/Match.lean
Lines 764 to 765 in d33f7c7
We have added a few kernel extensions that make assumptions about the Nat
and String
types. For example, the kernel assumes the term Expr.lit (literal.natVal 0)
has type Nat
. So, in principle, adversarial users may try to create their own Core.lean
(using prelude
) where Nat
is, for example, the empty type. Right now, we do not have protections against this kind of abuse. This is a very low priority issue, but it is important to document it.
There are many possible ways to fix this. For example, we can check in the Kernel whether Nat
and String
are the ones
we expect at addDecl
.
Lean tutorial https://leanprover.github.io/introduction_to_lean/ fails on "set_option profiler.freq 10"
Press "set_option profiler.freq 10" gives error
Expected behavior: No error
Actual behavior:
2:11:error: unknown option 'profiler.freq', type 'help options.' for list of available options
Done(0.001sec)
Reproduces how often: [100%
https://leanprover.github.io/introduction_to_lean/
Reproduced in browsers on two separate machines
Under certain (entirely pure) circumstances, a match
seems to go down the wrong branch.
https://gist.github.com/dselsam/bc46a2e3fb1d61929bc56b26f2f25568
Expected behavior:
[CONST(1), APP, APP]
Actual behavior:
[CONST(1), APP, CONST(2)]
Reproduces how often:
Every time.
Lean (version 4.0.0, commit bb8b13d, Release)
Ubuntu 18.04.2 LTS
Many minor changes to the function cause it behave correctly.
The linter should report problems such as:
macro "foo!" x:term y:term : term => `($x + $y)
#check foo! 10 20
#check 10 -- we get 'expect term' error at `#check`
The macro foo!
is accepted, but we get an error when we use it, and the error "expected term" is reported at #check 10
. Issue: 10 20
is parsed as (10 20)
because of the app
parser. So, any macro containing two consecutive term arguments with precedence < max
in the first argument produces this error. The linter should suggest the user include the max
precedence at x:term
.
macro "foo!" x:term:max y:term : term => `($x + $y)
Under certain circumstances, a
match t with
| c1 => ...
| c2 => ...
seems to go down both branches. If t
is printed in a dbgTrace
though, only the correct match fires.
Expected behavior:
It should print out "APP" only, and return the empty list.
Actual behavior:
It prints out "CONST" and "APP" before returning the empty list.
Reproduces how often:
Every time.
Lean (version 4.0.0, commit bb8b13d, Debug)
Small repro:
def f {α} : List α → Nat
| [a] => 1
| _ => 0
#check f.match_1
It produces panic error messages at skippingBinders
. I think we should use the default application delaborator at delabAppMatch
if the matcher is partially applied, i.e., it is missing the motive, discriminants or alternatives.
There are many scenarios we want to support where we need to update the parsing table while we are parsing.
Examples:
1- def
+ notation
macro that allows us to define functions and notation simultaneously.
def (_++_) {a} : List a -> List a -> List a
| [], bs => bs
| a::as, bs => a :: (as ++ bs)
2- Recursive macros. The following macro definition works as expected
syntax "repeat " tactic : tactic
macro_rules
| `(repeat $tac) => `(tactic| ($tac; repeat $tac) <|> skip)
but, the following one does not
macro "repeat " x:tactic : tactic => `(($x; repeat $x) <|> skip)
The problem is that the syntax repeat x
does not exist yet when we are parsing `(($x; repeat $x) <|> skip)
partial def foo : ∀ (n : Nat), State Unit Unit
| n =>
if n == 0 then pure () else
match n with
| 0 => pure ()
| n+1 => foo n
Produces:
LEAN ASSERTION VIOLATION
File: /home/dselsam/omega/lean4/src/library/compiler/csimp.cpp
Line: 1477
nparams <= k_args.size()
(C)ontinue, (A)bort/exit, (S)top/trap
on Debug build of a1bc316
set_option pp.all true in
#check (Sum.inl 1 : Sum Nat Bool)
produces
@Sum.inl.{0, } Nat Bool 1 : Sum.{0, } Nat Bool
macro m n:ident : command => `(def $n := 1)
does not work because the ident
n
is inserted in term
position. It should be $n:ident
. macro
could automate this; I don't think it would ever be the wrong thing to do.
I can implement this, though low priority atm.
There appears to have been a regression in the pattern compiler sometime in the last few weeks. Pulling a recent lean caused me to start seeing an error produced in code that previously (modulo some syntactic changes) would be accepted.
bugmin.lean
file via:LEAN_PATH=/usr/local/lib/lean/library:. /usr/local/bin/lean --make bugmin.lean
Expected behavior:
File should compile without errors.
Actual behavior:
Lean complains:
bugmin.lean:37:4: error: unknown free variable: _fresh.4.2315
Reproduces how often:
100% reproducible. However, the error is very fragile under code changes; removing apparently-redundant pattern matches or monadic binds, or even changing the constant nat value in the affected pattern matches can cause the problem to disappear.
$ lean --version
Lean (version 4.0.0, commit 4b49aa4b5040, Release)
macOS 10.14.6.
Github doesn't accept .lean
files, so rename...
bugmin.lean.txt
Given the definition
def foo : Nat -> Nat -> Nat -> List Nat
| _, _, 0 => [1]
| 0, _, _ => [2]
| n, d, k+1 => foo n d k
the equation compiler produces the incorrect error message.
-- error: equation compiler error, equation #2 has not been used in the compilation (possible solution: delete equation)
The bug is that the equation compiler has multiple steps. In this example, it first applies structural_rec
to eliminate the recursion. The third parameter is selected to justify why the recursion terminates, and the second equation is split into two because the third argument is variable here, but a pattern in other equations.
def foo : Nat → Nat → Π (a : Nat), Nat.below a → List Nat
| _x, _x_1, 0, _F := 1::List.nil
| 0, _x, 0, _F := 2::List.nil
| 0, _x, Nat.succ n, _F := 2::List.nil
| n, d, k+1, _F := (_F.fst).fst n d
The split is not communicated to the next step elim_match
that performs pattern matching.
The new second equation is not used and elim_match
incorrectly reports the error.
This bug will be fixed in the new equation compiler that we will implement in Lean.
In the meantime, we can avoid this issue by writing the definition as.
def foo : Nat -> Nat -> Nat -> List Nat
| _, _, 0 => [1]
| 0, _, Nat.succ _ => [2]
| n, d, k+1 => foo n d k
Example to reproduce bug
new_frontend
def foo
#exit -- as expected, we get the "expected := or |" error here, but error recovery swallows the `#exit`, and keep reporting the following errors
def bla :=
sss..
It should behave like the Haskell where
, and handle cases such as
def f : Nat -> Nat
| 0 => g 0
| x+1 => g (f x)
where g (x : Nat) := x + 1 -- the scope of `g` is the whole definition.
Many builtin tactics (e.g., cases
) are implemented using other tatics (e.g., induction
, subst
, ...). For these tactics, the error produced may often be counter-intuitive to users. Here is an example:
theorem ex (n : Nat) (h : n + 1 = n) : False := by
cases h;
done
produces the following error at cases
error: tactic 'subst' failed, 'n' occurs at
Nat.succ (Nat.add n 0)
case refl
n : Nat
h : n + 1 = n
h✝ : n = Nat.succ (Nat.add n 0)
⊢ h ≅ Eq.refl (n + 1) → False
A simple solution is to add catch
at cases
, and add more information. Example:
error: tactic `cases` failed
nested error: tactic 'subst' failed, 'n' occurs at
Nat.succ (Nat.add n 0)
case refl
...
@Kha What do you think?
The new naming convention makes the Has
prefix unnecessary (e.g., HasAdd
, HasToString
).
The Has
is a legacy from the Lean3 naming convention.
Moreover, we have already been dropping the Has
prefix in new code (e.g, we use ToExpr
instead of HasToExpr
).
We should use the parenthesizer and formatter in Syntax
objects before we print them. We should also hide macro scopes.
Example:
set_option pp.macroStack true
def f (x : List String) :=
if x + 1 > 0 then 1 else 2
One of the error messages is
error: failed to synthesize instance
HasOfNat (List String)
with resulting expansion
Greater._@._internal._hyg.0 x + 1 0
while expanding
x + 1 > 0
while expanding
if x + 1 > 0 then 1 else 2
In the message, Greater._@._internal._hyg.0 x + 1 0
should be printed as Greater✝¹ (x + 1) 0
.
Here is the ideal place to invoke formatter, parenthesizer, ...
Lines 72 to 73 in d33f7c7
@Kha We should make sure that sanitized names in the Syntax
object (e.g., Greater✝¹
) do not collide with sanitized names at ctx.lctx
.
This breaks in both the old and new frontend. Is it a bad idea? It seems to work in Lean 3.
abbrev DelabM := Id
abbrev Delab := DelabM Nat
example : DelabM Nat := pure 1 -- works
example : Delab := pure 1 -- doesn't work
When we write
@[builtinTermElab byTactic] def elabByTactic : TermElab :=
...
The attribute builtinTermElab
has to resolve the kind byTactic
.
The current implementation uses a primitive only available in the old frontend.
Line 75 in d33f7c7
OpenDecl
.Line 97 in d33f7c7
CoreM
here:lean4/src/Lean/KeyedDeclsAttribute.lean
Line 138 in d33f7c7
Possible solutions:
1- Include (currNamespace : Name) (openDecls : List OpenDecl)
at CoreM
. This solution is a bit wierd since this information is irrelevant for all other CoreM
and MetaM
methods.
2- Define a custom monad for Attribute
on top of CoreM
. This custom monad would have extra context containing scope information.
Solution 2 seems to be the way to go since we want to add support for scoped attributes in the future.
There are a few places it would be nice to have "composite error messages" that refer to many different locations. This happens when we tried different approaches to do something and each one of them failed in a different location. Examples: overloaded notation and showing a function terminates. We currently use two workarounds but none of them are ideal.
1- For overloaded notation, we group the error messages for each failure into a single message at the head symbol. This is not perfect since the position for each failure is lost.
2- For showing termination, we just say we failed, and tell the user to enable trace messages for inspecting why the different approaches failed. Here we preserve position information in the trace messages, but it is inconvenient to use since users have to go and add a set_option trace...
I think the ideal solution is to allow a Message
to contain nested messages. When displaying errors, we indent the nested messages. The IDE integration should be adjusted to allow us to click on the nested position and jump to it.
@Kha What do you think?
Originally from module.cpp
(RIP)
Persistent set_option
. We want to be able to store the option settings in .olean files.
The main issue is conflict between imported modules. That is, each imported module wants to
set a particular option with a different value. This can create counter-intuitive behavior.
Consider the following scenario
A.olean
: sets option foo
to trueB.olean
: imports A.oleanC.olean
: sets option foo
to falseD.lean
containing the following import clause:
import B C A
foo
is set to true since A
is the last module to be imported,B
is imported first, then A
(which sets option foo
to true),C
(which sets option foo
to false), the last import A
is skipped since A
has alreadyfoo
set to false.To address this issue we consider a persistent option import validator. The validator
signs an error if there are two direct imports which try to set the same option to different
values. For example, in the example above, B
and C
are conflicting, and an error would
be signed when trying to import C
. Then, users would have to resolve the conflict by
creating an auxiliary import. For example, they could create the module C_aux.lean
containing
import C
set_option persistent foo true
and replace import B C A
with import B C_aux A
Removing attributes. The validation procedure for persistent options can be extended to attribute deletion. In the latest version, we can only locally remove attributes. The validator for attribute deletion would sign an error if there are two direct imports where one adds an attribute [foo]
to a declaration bla
and the other removes it.
Parametric attributes. This is not a missing feature, but a bug. In the current version, we have
parametric attributes and different modules may set the same declaration with different parameter values.
We can fix this bug by using an attribute validator which will check parametric attributes, or we can allow parametric attributes to be set only once. That is, we sign an error if the user tries to reset them.
Suppose we want to match the match
syntax.
| `(match $discr:matchDiscr* $type:typeSpec* with | $alts:matchAlt*) =>
Note that it is already using the counterintuitive trick $type:typeSpec*
to handle optType
.
def typeSpec := parser! " : " >> termParser
def optType : Parser := optional typeSpec
The pattern is almost correct. The problem is the |
. It is optional. We currently don't have a way to handle it without the pattern twice: with and without the |
.
Any(?) use of #eval
currently breaks lean4-mode
because it generates invalid JSON:
#eval 33
$ bin/lean --json scratch.lean
33{"caption":"eval result","end_pos_col":8,"end_pos_line":1,"file_name":"/home/sebastian/lean/lean/scratch.lean","pos_col":0,"pos_line":1,"severity":"information","text":""}
@cipher1024 I'm afraid your recent changes to IO.println
broke this because #eval
depends on redirecting std::cout
:
lean4/src/frontends/lean/builtin_cmds.cpp
Line 386 in 6702434
MeasureType
, relation on MeasureType
, WellFounded MeasureType
, and tactic for discharging "decreasing conditions"Measure
for each function in a mutual block. It includes nested let rec
s.PreDefinition
=> kernel Declaration
We currently lose all trace messages when going through the PPExt indirection layer. While the indirection still makes sense even in the new frontend to avoid a dependency cycle, we should change the base monad after removing the old frontend.
In the old frontend, we have 3 elaboration function strategies for applications:
elabWithExpectedType
elabSimple
elabAsEliminator
The elabSimple
is essentially a workaround for issues in the old frontend. However, elabAsEliminator
is useful.
We should support it in the new frontend. We should also allow users to define new strategies in Lean. That is, user-defined functions with type:
(f : Expr) -> (namedArgs : Array NamedArg) -> (args : Array Arg) -> (expectedType? : Option Expr) -> TermElabM Expr
MacroM
is defined at src/Init
, but our tracing infrastructure is defined at src/Lean
. So, we don't have support for tracing at MacroM
.
@Kha when panic
is evaluated by the interpreter, the execution is interrupted as expected.
However, all trace messages produced using dbgTrace
are lost because the #eval
command implementation redirects stdout to a buffer.
Not sure what the best fix is. Here are some alternatives:
1- We register finalizers for panic
. Then, #eval
can set a finalizer that just dumps any intermediate output to stdout before terminating the execution.
2- We throw a C++ exception at panic
instead of aborting. We will leak memory, but #eval
will be able to dump the output as trace messages, and then terminate the Lean process with a panic message.
3- We don't change panic
, but the interpreter intercepts it and uses a different implementation. Example: store error message, and continue the execution with the "arbitrary" element. Pro: no leaks. Cons: the computation is nonsense after the first panic, and it may diverge.
Finish Structural.lean
Repro:
import Lean
new_frontend
open Lean
set_option trace.Meta.debug true
def test1 : MetaM Unit :=
trace! `Meta.debug (mkLambda Name.anonymous BinderInfo.default (mkSort levelZero) (mkBVar 0))
#eval test1 -- [Meta.debug] fun ([anonymous] : Prop) => [anonymous]
import Init.Lean
new_frontend
open Lean
#check mkNullNode -- Lean.Syntax
#check mkNullNode #[] -- Lean.Syntax
#check @mkNullNode -- Lean.Syntax
tests/compiler/qsortBadLt.lean
compiles to a 26MB binary because it uses Lean.mkAppStx._closed_9
, an extraction of the empty array!
The following code produces a segfault in the interpreter
def mkNatRef : IO (IO.Ref Nat) :=
IO.mkRef 0
@[init mkNatRef]
constant myRef : IO.Ref Nat := arbitrary _
def tst : IO Unit := do
myRef.modify Nat.succ;
myRef.get >>= IO.println
#eval tst
Bound variables are being pretty printed as «#».«0»
.
Repro:
import Lean
new_frontend
open Lean
def test : MetaM Unit :=
trace! `Meta.debug (mkBVar 0)
set_option trace.Meta.debug true in
#eval test
produces
[Meta.debug] «#».«0»
#eval show CoreM Unit from do
(← getEnv).constants.fold _ _
stdin:12:30: error: don't know how to synthesize placeholder
context:
a✝ : Environment
⊢ ReaderT Core.Context (StateRefT' IO.RealWorld Core.State (EIO Exception)) Unit
stdin:12:28: error: don't know how to synthesize placeholder
context:
a✝ : Environment
⊢ ReaderT Core.Context (StateRefT' IO.RealWorld Core.State (EIO Exception)) Unit →
Name → ConstantInfo → ReaderT Core.Context (StateRefT' IO.RealWorld Core.State (EIO Exception)) Unit
After that we could delete the old one
IO
(and EIO
) internal implementation is still transparent.
Lines 15 to 28 in 151e877
IO.RealWorld
.
@Kha this is not a high priority issue, but I can see users complaining about this all the time.
We can seal the implementation using the same approach we used to seal EnvExtension
:
lean4/src/Lean/Environment.lean
Lines 142 to 149 in 151e877
lean4/src/Lean/Environment.lean
Lines 239 to 249 in 151e877
An antiquotation such as $e
in term position can be parsed by all specific term parsers, so it produces a huge choice
node. While the quotation compiler can handle this, we should optimize the intermediate syntax tree by parsing the antiquotation earlier, right inside the Pratt parser before selecting a specific term parser.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.