leanprover-community / lean Goto Github PK

as reported on Zulip. This is a well known old bug, it shouldn't be hard to fix.

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

def int.pow_nat : ℤ → ℕ → ℤ
| (int.of_nat b) e := int.of_nat (b ^ e)
| (int.neg_succ_of_nat b) 0 := 1
| (int.neg_succ_of_nat b) (k+1) := (int.neg_succ_of_nat b) * int.pow_nat (int.neg_succ_of_nat b) k

instance int_has_pow_nat : has_pow int nat := ⟨int.pow_nat⟩

def int.pow (b : ℤ) : ℤ → ℤ
| (int.of_nat n) := b ^ n
| (int.neg_succ_of_nat n) := 0

instance : has_pow int int := ⟨int.pow⟩

@[simp]
def int.pow_of_nat (b : ℕ) (e : ℕ) : int.pow b e = int.of_nat (b ^ e) := rfl
-- 15:5: kernel failed to type check declaration 'int.pow_of_nat' this is usually due to a buggy tactic or a bug in the builtin elaborator
-- elaborated type:
--   ∀ (b e : ℕ), int.pow ↑b ↑e = int.of_nat (b ^ e)
-- elaborated value:
--   λ (b e : ℕ), rfl
-- nested exception message:
-- type mismatch at definition 'int.pow_of_nat', has type
--   ∀ (b e : ℕ), int.pow ↑b ↑e = int.pow ↑b ↑e
-- but is expected to have type
--   ∀ (b e : ℕ), int.pow ↑b ↑e = int.of_nat (b ^ e)

Expected behavior: either it passes, or I get type mismatch

Actual behavior: I get an error message complaining about a possible bug

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

$ lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 16.04.6 LTS
Release:        16.04
Codename:       xenial
$ uname -a
Linux jgross-Leopard-WS 4.4.0-161-generic #189-Ubuntu SMP Tue Aug 27 08:10:16 UTC 2019 x86_64 x86_64 x86_64 GNU/Linux

@cipher1024 asked me to report this error. (I assume this is the right place, but I'm not certain.)

In short, if one runs this

meta def foo: lean.parser unit :=
do
   return ()

run_cmd foo

the run_cmd line will return this unhelpful error:

vm check failed: dynamic_cast<vm_State*>(to_external(o)) (possibly due to incorrect axioms, or sorry)

As explained to me by Sebastian Ullrich, here:

That's a bug, run_cmd should only accept tactics. lean.parser cannot be used outside of user-defined parser extensions (notations/commands/tactic params).

In an editor, put the following in a Lean file:

def bar := ()

run_cmd
   unsafe_run_io $ do
   { io.env.get_cwd >>= io.print_ln,
     io.env.set_cwd "foo",
     io.env.get_cwd >>= io.print_ln }

/some/path/
/some/path/foo/

without restarting the Lean server, comment out the bar definition:

-- def bar := ()

run_cmd
   unsafe_run_io $ do
   { io.env.get_cwd >>= io.print_ln,
     io.env.set_cwd "foo",
     io.env.get_cwd >>= io.print_ln }

/some/path/foo/
/some/path/foo/foo/

Lean uses timestamps to check the validity of olean files, which causes trouble with some of the scripts that distribute oleans: the timestamps can get mangled and cause recompilation.

I did some quick experiments with this setup, where a --> b means a.lean imports b.lean:

three --> two --> one

I built all .olean files, then touched one.olean. Running lean three.lean recompiled two.lean, since the timestamp of one.olean is newer than that of two.olean.
Then I touched one.lean. Running lean three.lean recompiled one.lean, since the timestamp of one.lean is newer than that of one.olean. (It also recompiled two.lean of course.)

Naively, one of these checks should be easy to get rid of. Instead of comparing the timestamps of one.lean and one.olean, could we store the file hash of one.lean in the olean file? one.olean would be valid for one.lean iff the hashes match. This way, the lean files could have newer timestamps without causing issues.

The other one I'm less sure about. oleans know their direct imports, right? Could they store hashes of the oleans they import for the same kind of comparison?

Note: I'm not actually sure which kind of comparison causes the trouble with cache-olean/update-mathlib, or if both do.

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

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

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

I was unable to build Lean on i686 architecture using gcc versions > 6.5.0. This looks definitely like gcc bug so it's unclear if Lean developers could do something about it. Those gcc versions could be blacklisted on 32-bit architecture, though. That would make life of ordinary users and Linux packagers easier.

Steps to Reproduce

1. Use any gcc version greater than 6.5.0.

Expected behavior:

Actual behavior:

/bin/ld: shared_test: hidden symbol `__divmoddi4' in /lib/gcc/i686-unknown-linux-gnu/7.4.0/libgcc.a(_divmoddi4.o) is referenced by DSO

Reproduces how often:
I've tried gcc 6.5.0, 7.4.0 and 8.3.0. Only gcc 6.5.0 works fine.

Versions

Lean 3.4.2 and master (3.5.0). I'm on NixOS 19.03 i686.

Additional Information

Also, I don't know how critical this shared_test is. If possible it could be skipped on 32-bit.

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

The issue template gives links to https://github.com/leanprover/lean, not https://github.com/leanprover-community/lean. Is this deliberate?

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.
  • Reduced the issue to a self-contained, reproducible test case.

Description

equation compiler failed to prove equation lemma (workaround: disable lemma generation using `set_option eqn_compiler.lemmas false`) in the following code snippet. Found by @rwbarton.

Steps to Reproduce

variables (C D : Type) (c : C) (d : D)
inductive time : Type
| start {} : time
| after : (D → time) → time

-- set_option eqn_compiler.lemmas false
def foo : time D → Σ (γ : Type), γ → C
| time.start := ⟨C, id⟩
| (time.after ts) := ⟨(∀ (i : D), (foo $ ts i).1) × D, λ p, (foo $ ts p.2).2 $ p.1 p.2⟩

Versions

Lean (version 3.4.2, commit cbd2b6686ddb, Release)

Additional Information

• Here is a very similar case that work:

variables (C D : Type) (c : C) (d : D)
inductive time : Type
| start {} : time
| after : (D → time) → time

-- set_option eqn_compiler.lemmas false
def foo : time D → Σ (γ : Type), γ → C
| time.start := ⟨C, id⟩
| (time.after ts) := ⟨(∀ (i : D), (foo $ ts i).1) × D, λ p, (foo $ ts d).2 $ p.1 d⟩

• If you run #print foo.equations._eqn_1 there are two problems: the LHS is not applied to enough arguments (it should be applied to time.start) and the RHS seems to be a metavariable.
• @rwbarton and I find the code in function mk_lemmas in file src\library\equations_compiler\structural_rec.cpp suspicious.

Description

It seems that Lean does not correctly report type checking times. I'm not a 100% sure about this, so I'm making this issue partly to confirm. What I think happens:

1. "type checking" is measured with a time_task here. It's a RAII-style thing that prints out its measured timespan in the destructor. The variable is not passed anywhere, so the destruction happens right after return.
2. This means that the only measured statement is ::lean::check, defined here.
3. The immediately argument to check is always false (see type_checker.h and all uses of check), so the call to check_definition, which is what actually checks the type is deferred to happen in an asynchronous task-closure. The closure runs sometime after lean::check, which returns immediately.
4. Hence, the time measured by the time_task is merely the time to build the closure, potentially orders of magnitude less than type checking really takes.

Reproducing

1. Create profile.lean with contents:

import tactic.interactive tactic.ring tactic.ring2

constants (α : Type) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 : α)

theorem profile_me [comm_ring α]
  : ((((((((x15*x0)*x3)+x2)+x6)*(15: α))*x5)+x5)*(0: α))
  = ((0: α)*(1*((x5*1)+(x5*(1*((0+(15: α))*((x6*1)+(0+(x2+(1*(x3*((0+x0)*(x15*1)))))))))))))
:= by ring

2. Run lean -j1 --profile profile.lean in a debugger and inspect the control flow. Or put a print statement in the checked_proof closure and see that it prints long after "type checking of profile_me took ..".

Versions

Any recent one.

The equation compiler fails on mutual definitions that don't call each others, but only in meta lean.

--this works
mutual def f1, g1
with f1 : unit → unit
| () := ()
with g1 : unit → unit
| () := ()

--this works too
meta mutual def f2, g2
with f2 : unit → unit
| () := ()
with g2 : unit → unit
| () := f2 ()

--this doesn't:
--unexpected error, failed to generate equational lemmas in the front-end
meta mutual def f3, g3
with f3 : unit → unit
| () := ()
with g3 : unit → unit
| () := ()

To configure mathlib to use 3.5.0, we set in the toml file lean_version = "leanprover-community/lean:3.5.0". This lets leanpkg find the right version, but it complains:

WARNING: Lean version mismatch: installed version is 3.5.0, but package requires leanprover-community/lean:3.5.0

A few possible solutions:

• We can change https://github.com/leanprover-community/lean/blob/master/leanpkg/leanpkg/main.lean#L17 to split on : and only compare the rhs
• We maybe could change the version name to leanprover-community/lean:3.5.0? I'm not sure this would work.

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

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

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

[Description of the issue]
Does the static version is supposed to work? I'm getting a crash in compilation.

Steps to Reproduce

1. cmake -DSTATIC=ON

Expected behavior: [What you expect to happen]
Compilation should finish successfully.

Actual behavior: [What actually happens]
[CMakeFiles/standard_lib.dir/build.make:57: CMakeFiles/standard_lib] Segmentation fault

Reproduces how often: [What percentage of the time does it reproduce?]
All the time.

Versions

GitHub master branch revision 8c2470b755c4ab8cf983ed024c1150fbf01e8822. I'm on NixOS 19.03 i686.

Additional Information

I suspect that it might work on x86_64 but didn't try it.

I added docs for mathlib's #where command today, and it occurred to me that it should really be implemented natively in 3.5c. The current version gives a reasonable approximation of the info you want to see, but it's not really reliable. Even if we don't move mathlib to 3.5c (I think we should soon), it's a transient command, so it wouldn't break anything.

(I'm not planning to implement this myself, but it might be a nice little project if anyone is interested.)

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

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

It has been noted by Abel and Coquand in a recent preprint that Lean's type theory allows looping proof terms. See also here for more discussion. It is unclear what effect this has on typechecking, but in principle it shouldn't matter -- the only terms that we can get to loop are proofs, i.e. have types in Prop. Proof irrelevance states that any two proofs of the same proposition are definitionally equal, so there should be no need to reduce any proof terms in order to check them for equality, since the proof-irrelevance rule always applies.

Sadly, the elaborator does not always deal with this properly and fixing that is the actual target of this issue. In current Lean (537f489), the following bit of code goes into an infinite loop in the elaborator:

def top := ∀ p : Prop, p → p
def pext := ∀ (A B : Prop), A → B → A = B
def supercast (h : pext) (A B : Prop) (a : A) (b : B) : B
  := @cast A B (h A B a b) a
def omega : pext → top :=
  λ h A a, supercast h (top → top) A
    (λ z: top, z (top → top) (λ x, x) z) a
def Omega : pext → top :=
  λ h, omega h (top → top) (λ x, x) (omega h)
def Omega' : pext → top := λ h, (λ p x, x)

theorem loopy : Omega = Omega' := rfl -- loops

A naive solution to this which seems not to break other aspects of elaboration is to add a proof-irrelevant (is_def_eq_proof_irrel) equality check before delta-reduction in type_context::is_def_eq_core_core. This prevents definitions from being unfolded in proofs and stops the elaborator loop in the above code, but a fully unfolded term:

theorem loopy : (λ h, (λ h A a, (λ (h': (∀ (A B : Prop), A → B → A = B)) T U t u, (λ α β (h: α = β) (a: α), (eq.rec a h: β)) T U (h' T U t u) t) h ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) A (λ z: (∀ p : Prop, p → p), z ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) (λ x, x) z) a) h ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) (λ x, x) ((λ h A a, (λ (h': (∀ (A B : Prop), A → B → A = B)) T U t u, (λ α β (h: α = β) (a: α), (eq.rec a h: β)) T U (h' T U t u) t) h ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) A (λ z: (∀ p : Prop, p → p), z ((∀ p : Prop, p → p) → (∀ p : Prop, p → p)) (λ x, x) z) a) h)) = (λ h, (λ p x, x)) := rfl

still gets stuck repeatedly calling type_checker::infer_type_core. At the moment I am unsure how to fix the latter. There is also the question of whether we want to fix it, i.e. prevent the elaborator from reducing proofs, in the first place -- as Mario mentioned, perhaps Turing-complete computation can be useful in proofs.

Last month, the issues were disabled in the leanprover/lean repository. Would it be possible to get them copied to this repository? There was a little discussion here.

Zulip topic: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Bug.20with.20let.20in.20pattern.20match

def h : ℕ → bool
| 0 := let _ := tt in tt
| (k+1) := k = k -- fails
--| (k+1) := if k = k then tt else ff -- fails
--| (k+1) := if h : k = k then tt else ff -- succeeds

The let in the first case seems to prevent type class resolution from finding decidable (k = k) in the second. Weirdly, if you use a dependent if and name the k = k hypothesis, it succeeds. It has to be a destructive let, i.e. let a := tt in tt succeeds.

Mario notes that to_bool (k = k) succeeds, pointing to something low-level going on.

Fixing this isn't high priority, just wanted to document what seems to be an unfamiliar bug.

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

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

When I follow the instructions to build from source (on Fedora), I get

cmake ../../src -DCMAKE_INSTALL_PREFIX=/opt/lean/v3.4.2 -DCMAKE_BUILD_TYPE=RELEASE
make -j
...
Scanning dependencies of target standard_lib
/home/waldmann/software/prover/lean/library/init/meta/tactic.lean: parsing at line 1399terminate called after throwing an instance of 'lean::exception'
  what():  vm check failed: is_composite(o) (possibly due to incorrect axioms, or sorry)
make[2]: *** [CMakeFiles/standard_lib.dir/build.make:57: CMakeFiles/standard_lib] Aborted (core dumped)
make[1]: *** [CMakeFiles/Makefile2:954: CMakeFiles/standard_lib.dir/all] Error 2
make: *** [Makefile:163: all] Error 2

most of the time. This happen with gcc (GCC) 9.2.1 20190827 (Red Hat 9.2.1-1)

The build works with

• gcc (Ubuntu 7.4.0-1ubuntu1~18.04.1) 7.4.0
• clang version 9.0.0 (Fedora 9.0.0-1.fc31)
• g++ (GCC) 9.2.0 (built from source) (on Fedora)

import data.rat
import data.vector

def E {n} (l : vector rat n) : rat := list.foldl (+) 0 l.val / n

I can't get foldl to show up in autocomplete. That same goes for val. data.vector and data.rat are from the mathlib. I am using VS Code with Windows 10. Lean version 3.42.

Reposted from here and here.

People ask if you can do this a lot, and it could help other things too (e.g. leanprover-community/mathlib#946)

Reported by @CohenCyril on Zulip. This code (which relies on the add_ginductive hook added in #3), crashes the latest nightly:

open expr tactic

run_cmd do
  let ty : expr := sort level.zero,
  updateex_env $ λe,
    e.add_ginductive options.mk [] [ty] [(("test", ty), [])] ff

This assert:

fails when running the debug build. The backtrace indicates that it results from this:

The following is fine (deleting the first ty from the final line):

open expr tactic

run_cmd do
  let ty : expr := sort level.zero,
  updateex_env $ λe,
    e.add_ginductive options.mk [] [] [(("test", ty), [])] ff

Is lstlean.tex in this repo the most up-to-date version of this file? I have accumulated some local changes over time, should I make a PR to add them to this file?

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

The file generated by the command line argument --doc is empty.

Steps to Reproduce

1. Create file doc.lean with some doc strings.

namespace test

/-- docs for the win! -/
lemma abc : true := true.intro

end test

2. Run lean --doc=doc.out doc.lean
3. Check that doc.out is empty

Expected behavior: doc.out should contain some documentation?

Reproduces how often: Always

Versions

Lean (version 3.4.2, commit cbd2b66, Release)
on Ubuntu 18.04 x64

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

example : (0 : ℤ) = 0 :=
begin
  simp [has_zero.zero]
-- 4:1: (deterministic) timeout
end

Expected behavior: lean returns quickly

Actual behavior: lean times out

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

$ lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 16.04.6 LTS
Release:        16.04
Codename:       xenial
$ uname -a
Linux jgross-Leopard-WS 4.4.0-161-generic #189-Ubuntu SMP Tue Aug 27 08:10:16 UTC 2019 x86_64 x86_64 x86_64 GNU/Linux

def nat.foldl.fin.template {α : Type} : α := sorry
def nat.foldl.fin {α : Type} (f : α) : α := nat.foldl.fin.template

This works for me.

def nat.foldl.fin.template {α : Type} : α := sorry
def nat.foldl.fin {α : Type} : ∀ (f : α), α | f := nat.foldl.fin.template

This does not.

I am using Lean 3.42.

Reposted from here.

Reported by @Vtec234 on Zulip. The following code crashes both 3.4.2 and the latest 3.5.0c nightly ("nightly-2019-05-17"):

lemma segfault {α: Type u} {a a': α} (H : a = a') : a = a' := begin
  revert a a,
end

This does not crash when run in the web editor.

This is a tracking issue for cleaning up warnings in the lean build (or determining that they can't be fixed).

Create a new file in a Lean 3.4.2 or Lean 3.5.0 project with the following contents:

.

Open the file in VS Code and then add a new line after the period and the Lean server will crash. I'm also able to trigger a crash by simply moving the cursor around.

This seems to happen for any file ending in a period.

I've been unable to reproduce this from the command line. Can anyone check if this happens in Emacs as well?

First reported in Zulip by @alashworth here.

The following call to change is doing nothing.

example (P : ℕ → Prop) (h : ∀ n, P n) : true :=
begin
  change ∀ k, P k at h,
  trivial
end

Reported by @kodyvajjha on Zulip. The following code crashes both 3.4.2 and the latest 3.5.0c nightly ("nightly-2019-05-17"):

universe u

open nat

variable {α : Type u}
def vec : Type u → ℕ → Type*
| A 0 := punit
| A (succ k) := A × vec A k

inductive dfin : ℕ → Type
| fz {n} : dfin (n+1)
| fs {n} : dfin n → dfin (n+1)

def kth_projn : Π n, vec α n → dfin n → α
| (_) x dfin.fz := x.fst -- crashes lean
| (succ n) (x,xs) (dfin.fs k) := kth_projn n xs k

Curiously, it does not crash when run in the web editor, instead returns the following error message:

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
cases tactic failed, it is not applicable to the given hypothesis

Description

I am reliably unable to build the Lean standard library with a Release build of the master branch and get this error:

terminate called after throwing an instance of 'lean::exception'
  what():  vm check failed: is_composite(o) (possibly due to incorrect axioms, or sorry)

It also seems to happen on MinGW, and it has been mentioned on Zulip.

Using Lean in single-threaded (-j1) mode doesn't help, which makes me think this is not a race condition. Combined with the fact that both of

• building Lean in Debug mode
• using the Nightly binary from elan

do work, I'm thinking this is undefined behaviour that happens to work sometimes if the compiler does the right undefined thing.

Steps to Reproduce

1. Build Lean with -DCMAKE_BUILD_TYPE=RELEASE
2. Try to ../bin/lean --make in the library/ folder

Versions

Lean (version 3.5.0, commit 014fd37, RELEASE)
Arch Linux, GCC 9.1.0

Sometimes the macOS clang++ travis build fails during the ctest step in leantest_non_meta_rec_fn.lean like this:

379/1325 Test #283: leantest_non_meta_rec_fn.lean ...............................***Failed    0.05 sec

-- testing non_meta_rec_fn.lean

-- using result from test_all.sh

--- non_meta_rec_fn.lean.expected.out	2019-10-17 20:25:29.000000000 +0000

+++ non_meta_rec_fn.lean.produced.out	2019-10-17 20:34:55.000000000 +0000

@@ -1,4 +1,4 @@

-non_meta_rec_fn.lean:3:36: error: failed to prove recursive application is decreasing, well founded relation

+non_meta_rec_fn.lean:3:0: error: failed to prove recursive application is decreasing, well founded relation

   @has_well_founded.r true (@has_well_founded_of_has_sizeof true (default_has_sizeof true))

 Possible solutions: 

   - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.

ERROR: file non_meta_rec_fn.lean.produced.out does not match non_meta_rec_fn.lean.expected.out

It seems to happen randomly; I think I've seen it go away after the job was restarted.

cf. #69 (comment)

Here are a bunch of other instances I found in the travis "build history" tab which go back several months:

• https://travis-ci.org/leanprover-community/lean/jobs/599329732#L1895
• https://travis-ci.org/leanprover-community/lean/jobs/559029182#L4601
• https://travis-ci.org/leanprover-community/lean/jobs/594302054#L4955
• https://travis-ci.org/leanprover-community/lean/jobs/543879667#L4469
• https://travis-ci.org/leanprover-community/lean/jobs/542915441#L4462
• https://travis-ci.org/leanprover-community/lean/jobs/538388974#L4422

Mario helped me write a proof:

lemma foo (n k : ℕ) : k ≡ ((k / 2^n) + (k % 2^n)) [MOD 2^n - 1] :=
-- See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/help.20finding.20a.20lemma/near/177698446
begin
  conv {to_rhs, rw [← nat.mod_add_div k (2^n), add_comm]},
  refine nat.modeq.modeq_add _ (by refl),
  conv {to_rhs, skip, rw ← one_mul (k/2^n)},
  refine nat.modeq.modeq_mul _ (by refl),
  symmetry,
  rw [nat.modeq.modeq_iff_dvd, int.coe_nat_sub],
  exact nat.pow_pos dec_trivial _
end

in which both instances of to_rhs are a bit strange. The first one actually looks at the left-hand-side, while the second one requires a skip before actually reaching the right-hand-side.

Description

Changing sorry to {} below crashes the lean server in vscode and when compiling with lean --make Test.lean leads to

$ lean --make Test.lean
[1]    28677 segmentation fault (core dumped)  lean --make Test.lean

It only warns about the 'sorry' (and doesn't segfault) else.

Steps to Reproduce

I've uncommented some instances, they don't matter for the issue but might help with finding the bug.

universes u

inductive Incr (a : Type u) : Type u
| Z : Incr
| S : a -> Incr

instance incr_functor : functor Incr :=
  { map := λ α β f a, Incr.rec_on a (Incr.Z β) (Incr.S ∘ f) }

-- instance incr_functor_lawful : is_lawful_functor Incr :=
  -- { id_map := begin intros, simp, cases x, repeat { refl } end
  -- , comp_map := begin intros, simp, cases x, repeat { refl } end }

instance incr_has_bind : has_bind Incr :=
  { bind := λ _ _ a f, Incr.rec_on a (Incr.Z _) f }

instance incr_has_seq : has_seq Incr :=
  { seq := λ _ _ x y, Incr.rec_on x (Incr.Z _) (λ f, f <$> y) }

instance incr_has_pure : has_pure Incr :=
  { pure := λ _, Incr.S }

instance incr_applicative : applicative Incr := {}

-- instance incr_applicative_lawful : is_lawful_applicative Incr := 
  -- { pure_seq_eq_map := begin intros, simp end
  -- , map_pure := begin intros, simp [(<$>)], end
  -- , seq_pure := begin intros, simp [(<$>)], end
  -- , seq_assoc := begin intros, cases x, 
      -- repeat { cases g, repeat { cases h, refl, refl } } end }

instance incr_monad_real : monad Incr := sorry -- using {} segfaults lean :(

Expected behavior:
A valid monad instance

Actual behavior:
Segfault, see above.

Reproduces how often:
Always.

Versions

$ lean --version
Lean (version 3.4.2, commit 72a965986fa5, Release)

$ cat /etc/lsb-release             
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=19.04
DISTRIB_CODENAME=disco
DISTRIB_DESCRIPTION="Ubuntu 19.04"

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

Dowloading Lean Nightly on a Windows machine fails.

Steps to Reproduce

curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf \| sh  info: downloading installer                                                      Archive:  elan-init.zip                                                            inflating: elan-init.exe                                                                                                                                        Welcome to Lean!                                                                                                                                                  This will download and install Elan, a tool for managing different Lean          versions used in packages you create or download. It will also install a         default version of Lean and its package manager, leanpkg, for editing files not  belonging to any package.                                                                                                                                         It will add the leanpkg, lean, and elan commands to Elan's bin directory,        located at:                                                                                                                                                         C:\Users\sulli\.elan\bin                                                                                                                                        This path will then be added to your PATH environment variable by modifying the  HKEY_CURRENT_USER/Environment/PATH registry key.                                                                                                                  You can uninstall at any time with elan self uninstall and these changes will    be reverted.                                                                                                                                                      Current installation options:                                                                                                                                          default toolchain: stable                                                     modify PATH variable: yes                                                                                                                                       1) Proceed with installation (default)                                           2) Customize installation                                                        3) Cancel installation                                                           2                                                                                                                                                                 I'm going to ask you the value of each these installation options.               You may simply press the Enter key to leave unchanged.                                                                                                            Default toolchain? (stable/nightly/none)                                         nightly                                                                                                                                                           Modify PATH variable? (y/n)                                                      y                                                                                                                                                                                                                                                  Current installation options:                                                                                                                                          default toolchain: nightly                                                    modify PATH variable: yes                                                                                                                                       1) Proceed with installation (default)                                           2) Customize installation                                                        3) Cancel installation                                                           1                                                                                                                                                                 info: syncing channel updates for 'nightly'                                      info: latest update on nightly, lean version nightly-2019-11-01                  info: downloading component 'lean'                                               error: binary package was not provided for 'windows'                                                                                                              Press the Enter key to continue.
--

Expected behavior: Proper install

**Actual behavior:**fails

Reproduces how often: Student notified me, I tried it, saw same failure behavior.

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

3.4.2 nightly. Windows OS.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

The purpose of VM-overrides is to be able to replace non-meta code with more efficient meta code when evaluating in the VM. Some use cases:

• Write a formally verified version of floating point numbers but use native floats in the VM.
  The result is that users can use floats in non-meta code without the performance penalty.
• Make finsets evaluatable using native rb trees?
• Efficient linear algebra, matrices.
• Make it clear in the Lean init code when a function is being overridden by Lean.

Non-goals:

• No guarantees that the meta and non-meta interpretations do the same thing. VM evaluation can still have bugs which the kernel doesn't see.
• Some typechecking will be done but no guarantees that the override and original declaration are compatible.

Here is a use case of VM-overrides as discussed on Zulip.

-- These are implemented in C++ using native floats.
meta constant native.float : Type
meta constant native.float.add : native.float → native.float → native.float

inductive IEEE_float := ...

def IEEE_float.add := ...
-- plus other defininitions

meta constant native.float.to_IEEE : native.float → IEEE_float
meta constant native.float.of_IEEE : IEEE_float → native.float

-- No vm implementation needed
@[inline] meta def native.float.rec {C : Sort*}
  (H : IEEE_float → C) (f : native.float) : C :=
H f.to_IEEE

@[vm_override native.float] -- optional?
structure float := (to_IEEE : IEEE_float)

-- Override the core functions
attribute [vm_override native.float.rec] float.rec
attribute [vm_override native.float.of_IEEE] float.mk
attribute [vm_override native.float.to_IEEE] float.to_IEEE

@[vm_override native.float.add]
def float.add : float -> float - > float := \lam (mk x) (mk y), mk $ IEEE_float.add x y

-- No error because the equation compiler defines this function in terms of
-- float.rec and float.mk
def float.neg : float -> float  := \lam (mk x) , mk $ IEEE_float.neg x

-- This does not error because only composed of vm_overridden functions.
def float.double := \lam x , float.add x x

-- prints a big list `(float, native.float), (float.add, native.float.add), ...`
#print vm_override

-- prints a `native.float`
#print vm_override float.add

-- This _does_ error because the arities do not match up.
@[vm_override native.float.pow]
def float.square : float -> float := \lam (mk x), ...

Here are some loose ends from #17:

• There are a handful of tests that fail when running ctest with the emscripten build.

• If those get figured out, then as a followup we could look into adding back the tests to travis. A naïve approach takes way too long so we would have to break the emscripten build / test up into multiple phases. (See this comment).

• There are warnings coming from the recent vm_float feature (#2) that I haven't looked into:

emcc: warning: cannot represent a NaN literal '0x7fed6b0bae00' with custom bit pattern in NaN-canonicalizing JS engines (e.g. Firefox and Safari) without erasing bits!
in tail call fastcc void @_ZN4lean11mk_vm_floatEf(%"struct.std::__2::__compressed_pair_elem.26.1385"* noalias %0, float 0x7FF4000000000000) in _ZZN4lean19initialize_vm_floatEvENK3$_8clEv()

I'm planning a new community release of Lean and here are the features I would like to include

• Lean API to the equation compiler
• Lean API for creating mutually inductive and nested inductive types
• Lean API for overriding Lean definitions in the VM
• support for deployment in leanpkg (e.g. like update-mathlib and cache-olean)

• FFI with C / C++ / Rust / Python
• Lean plugins
• Code extraction

Merging the sockets PR broke the build https://travis-ci.org/leanprover-community/lean/builds/523525562. @khoek Please fix it

edit: I did the tests below in 3.4.2, the behavior in 3.5.1 is detailed in the following comment.

I think the following is an accurate description of the current state of affairs: inside a docstring, adding a language tag to a code block surrounded by triple-backticks leads to an error if there's any non-whitespace text after the final code block.

A few examples:

No error:

/-!
```lean
code
```
-/

This gives the error invalid doc string, end of code block ``` expected (but it shouldn't):

/-!
```lean
code
```
non-whitespace text afterwards
-/

This gives no error:

/-!
```
code
```
non-whitespace text afterwards
-/

This example also gives no error. Compare this example in mathlib's reassoc_tactic) (pointed out by @robertylewis):

/-!
```lean
code
```
non-whitespace text afterwards
```
more code
```
-/

This gives an error (but it shouldn't):

/-!
```lean
code
```
non-whitespace text afterwards
```
more code
```
more non-whitespace text
-/

Lean thinks this is OK, but it isn't:

/-!
```lean
code
```
non-whitespace text afterwards
```
-/

The error message comes from src/library/documentation.cpp.

Originally reported by @jcommelin on zulip.

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

This code fails:

example (n m : ℕ) : n + m = m + n :=
begin
let s := n + m,
induction n,
case nat.zero : {sorry}, -- error: could not find open goal of given case
case nat.succ : {sorry}
end

While this code succeeds:

example (n m : ℕ) : n + m = m + n :=
begin
-- let s := n + m,
induction n,
case nat.zero : {sorry}, -- error: could not find open goal of given case
case nat.succ : {sorry}
end

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.