leanprover / lean4 Goto Github PK

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?

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..

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

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.

Steps to Reproduce

1. Compile the attached 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.

Versions

$ lean --version
Lean (version 4.0.0, commit 4b49aa4b5040, Release)

macOS 10.14.6.

Additional Information

Github doesn't accept .lean files, so rename...
bugmin.lean.txt

After that we could delete the old one

• Syntax for specifying MeasureType, relation on MeasureType, WellFounded MeasureType, and tactic for discharging "decreasing conditions"
• Syntax for specifying Measure for each function in a mutual block. It includes nested let recs.
• PreDefinition => kernel Declaration
• Good default heuristics.

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

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.

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.

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

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.

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.

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.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Under certain (entirely pure) circumstances, a match seems to go down the wrong branch.

Steps to Reproduce

https://gist.github.com/dselsam/bc46a2e3fb1d61929bc56b26f2f25568

Expected behavior:

[CONST(1), APP, APP]

Actual behavior:

[CONST(1), APP, CONST(2)]

Reproduces how often:

Every time.

Versions

Lean (version 4.0.0, commit bb8b13d, Release)
Ubuntu 18.04.2 LTS

Additional Information

Many minor changes to the function cause it behave correctly.

Finish Structural.lean

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 |.

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean tutorial https://leanprover.github.io/introduction_to_lean/ fails on "set_option profiler.freq 10"

Steps to Reproduce

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%

Versions

https://leanprover.github.io/introduction_to_lean/

Additional Information

Reproduced in browsers on two separate machines

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)

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.

IO (and EIO) internal implementation is still transparent.

@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:

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

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]

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).

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?

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

@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.

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:

set_option pp.all true in
#check (Sum.inl 1 : Sum Nat Bool)

produces

@Sum.inl.{0, } Nat Bool 1 : Sum.{0, } Nat Bool

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.

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»

$ LEAN_PATH=Init=wrong bin/lean scratch.lean
[2]    24627 segmentation fault (core dumped)

This is because

/cc @cipher1024

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 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)

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, ...

@Kha We should make sure that sanitized names in the Syntax object (e.g., Greater✝¹) do not collide with sanitized names at ctx.lctx.

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.

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

tests/compiler/qsortBadLt.lean compiles to a 26MB binary because it uses Lean.mkAppStx._closed_9, an extraction of the empty array!

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 true
  • B.olean : imports A.olean
  • C.olean : sets option foo to false
  • We create D.lean containing the following import clause:

    import B C A
    

    The user may expect that foo is set to true since A is the last module to be imported,
    but this is not the case. B is imported first, then A (which sets option foo to true),
    then C (which sets option foo to false), the last import A is skipped since A has already
    been imported, and we get foo 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.

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

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.

Steps to Reproduce

1. Run the included build script:

leanbug.zip

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

Versions

$ lean --version
Lean (version 4.0.0, commit 52b86c3b4b7e, Release)

macOS 10.14.6

Additional Information

Maybe this is related to issues with filesystem case-sensitivity?

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.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

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.

Steps to Reproduce

1. Download the gist: https://gist.github.com/dselsam/95b2c833129a5661767ec64e7625e050
2. Build it and run it.

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.

Versions

Lean (version 4.0.0, commit bb8b13d, Debug)

Additional Information

We should support

• DecidableEq
• HasBeq
• HasToString
• Repr
• Inhabited
• ...

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: