This feature is needed when we declare an inductive predicate/type
which is indexed by a mutual and/or nested inductive datatype.
See tests/lean/run/term_pred.lean for an example.
@Armael: this commit should fix the issue with the `cases` tactic that
you reported today.
We want to make sure string users do not depend on the string
implementation. This is the first step.
We need this refactoring *now* to make sure it will not be
super painful to address issue #1175
The `unsafe_change e` tactic is similar to the `change e` tactic, but it
does not check whether `e` is definitionally equal to the current
tactic. It is useful when implementing tactics such as:
```
meta def dunfold : list name → tactic unit :=
λ cs, target >>= dunfold_core transparency.instances default_max_steps cs >>= unsafe_change
```
The tactic `dunfold_core` guarantees that the resultant expression is
definitionally equal to the input one.
This was one of the performance problems at issue #1646.
Here are the runtimes for size 7 in the example described at issue #1646.
Before this commit:
tactic execution took 4.96s
elaboration of some_lifted_lets took 7.6s
type checking time of some_lifted_lets took 31.1ms (aka QED time)
total execution time: 12.785s
After this commit:
tactic execution took 3.78s
elaboration of some_lifted_lets took 5.71s
type checking time of some_lifted_lets took 35.2ms
total execution time: 10.693s
Before this commit they were implemented using C++ and Lean.
A Lean procedure was being invoked for each subterm of the input term.
This is one of the performance problems at issue #1646.
Here are the runtimes for size 7 in the example described at issue #1646.
Before this commit:
tactic execution took 7.48s
elaboration of some_lifted_lets took 11.5s
type checking time of some_lifted_lets took 33.4ms (aka QED time)
total execution time: 16.841s
After this commit:
tactic execution took 4.96s
elaboration of some_lifted_lets took 7.6s
type checking time of some_lifted_lets took 31.1ms (aka QED time)
total execution time: 12.785s
This is one of the performance problems at issue #1646.
The method `local_context::erase_user_name(local_decl const & d)` was
inefficient when there are many locals with the same user facing name.
For size 7 in the example described at issue #1646, the average size of the
declaration list was 400. Here are the runtimes for size 7
Before: 19.021 secs
After: 16.433 secs
There are more performance issues.
They can be used to store user state in the tactic_state object.
@Armael @jroesch: The new file tests/lean/run/tactic_ref.lean contains a few examples.
We were getting the following error non deterministically:
```
library/init/data/nat/bitwise.lean:131:6: error: exact tactic failed, type mismatch, given expression has type
z = f ff 0 z
but is expected to have type
eq.rec z e = f ff 0 (binary_rec f z 0)
state:
C : ℕ → Sort u,
f : Π (b : bool) (n : ℕ), C n → C (bit b n),
z : C 0,
h : f ff 0 z = z,
b : bool,
n : ℕ,
b0 : bit b n = 0,
bf : bodd 0 = b,
n0 : shiftr 0 1 = n,
e : 0 = bit ff 0
⊢ eq.rec z e = f ff 0 (binary_rec f z 0)
```
This error was happening because of the type_context.unfold_lemmas new
flag. The type context thread local cache must be flushed whenever the
value of type_context.unfold_lemmas has changed.
This commit fixes issue #1631. However, it is not a perfect solution.
This commit improves the predicate that checks whether a definition is
noncomputable or not. This predicate was implemented before we had
a code generator.
We should refactor the code and use the code generator to check
whether a definition is noncomputable or not. Otherwise, we will
keep finding mismatches between the predicate at noncomputable.cpp
and what the code generator implements.
Older gcc compilers generate a warning when the attribute is used.
I found out that GCC 7 will not produce a warning if comments
such as /* fall-thru */ or /* FALLTHRU */ are used instead of the
attribute [[fallthrough]]
