Zulip Chat Archive

Stream: general

Topic: moving algebra out of core


Johan Commelin (May 11 2020 at 04:30):

Starting a new thread for this project.
Can someone explain me: when I build core

cd build/releases
cmake ../../src
make

How is this aware of any .lean files in core? I grepped through all the Makefiles, and they don't seem to mention lean files anywhere.

Johan Commelin (May 11 2020 at 04:31):

Or does it not care, but will you only notice once you run the tests if you've changed/moved a bunch of lean files?

Yury G. Kudryashov (May 11 2020 at 04:56):

Here is the relevant part of CMakeLists.txt:

add_custom_target(
    standard_lib ALL
    COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" --make ${LEAN_EXTRA_MAKE_OPTS}
    DEPENDS bin_lean
    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library"
    )

add_custom_target(
    leanpkg ALL
    COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" --make ${LEAN_EXTRA_MAKE_OPTS}
    DEPENDS standard_lib
    WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../leanpkg"
)

Yury G. Kudryashov (May 11 2020 at 04:57):

It just runs this command. It doesn't care what it does.

Johan Commelin (May 11 2020 at 04:57):

/me should learn cmake

Yury G. Kudryashov (May 11 2020 at 04:59):

BTW, @Gabriel Ebner do you want me to look at lean buildsystem? A few years ago I contributed several patches to cmake and to KDE cmake files.

Bryan Gin-ge Chen (May 11 2020 at 05:01):

If you only plan to edit Lean files, you can just mess around in library after compiling a binary from the latest commit.

Yury G. Kudryashov (May 11 2020 at 05:02):

In particular, writing build files to source tree is generally a bad idea. If I have two build directories with different configuration, then I expect these two builds to be completely independent.

Bryan Gin-ge Chen (May 11 2020 at 05:02):

Oh, maybe this post by Jason will help? It could be an alternate way to play around with library without having to build Lean.

Johan Commelin (May 11 2020 at 05:03):

But I guess I will have to touch .cpp as well. Cut norm_num away.

Yury G. Kudryashov (May 11 2020 at 05:04):

What should core know about natural and integer numbers? Only definitions of operations? Something else?

Johan Commelin (May 11 2020 at 07:40):

lean#224 is the first step

Johan Commelin (May 11 2020 at 07:59):

That PR removes all the CPP involving norm_num.

Johan Commelin (May 11 2020 at 07:59):

A follow-up PR should strip most algebra from the core library. But that lean code is pretty tangled )-;

Kenny Lau (May 11 2020 at 08:03):

/me is somewhat surprised that Lean code is faster than cpp code

Johan Commelin (May 11 2020 at 08:04):

That's fine

Gabriel Ebner (May 11 2020 at 08:20):

Yury G. Kudryashov said:

BTW, Gabriel Ebner do you want me to look at lean buildsystem? A few years ago I contributed several patches to cmake and to KDE cmake files.

Are you talking about removing the part that copies lean to bin/lean? I've already gotten used to this horrible hack. I don't think that there's an immediate need to change it. See also previous discussion here: https://github.com/leanprover/lean/issues/1918

Gabriel Ebner (May 11 2020 at 08:29):

Yury G. Kudryashov said:

What should core know about natural and integer numbers? Only definitions of operations? Something else?

It needs a few lemmas for the equation compiler. If you write match n with 314 := a | 42 := b | _ := c end, then it needs to prove that 314 ≠ 42. The definitions of natural numbers (including exponentiation) are also required for the VM (because they are overriden) and the tactic framework.

Mario Carneiro (May 11 2020 at 09:07):

@Kenny Lau The reason it's faster is because the C++ is using instance search and norm_num is (now) aggressively caching. It turns out that actual number crunching was nothing compared to finding typeclasses

Johan Commelin (May 11 2020 at 09:45):

This is what we need to unclutter:
import_graph.pdf

Johan Commelin (May 11 2020 at 09:48):

@Mario Carneiro Do you know by heart whether something like init.meta.well_founded_tactics has to stay in core?

Mario Carneiro (May 11 2020 at 09:49):

that tactic is a mess, I'd like to see it gone

Mario Carneiro (May 11 2020 at 09:49):

it should be assumption

Johan Commelin (May 11 2020 at 09:53):

What does that mean for this project...

Mario Carneiro (May 11 2020 at 09:54):

It can definitely be removed from core

Johan Commelin (May 11 2020 at 09:55):

Ok, I'll try my best

Mario Carneiro (May 11 2020 at 09:56):

It is used by lean magic currently: if you leave off the using_well_founded clause in a well founded recursive definition, it will call the tactic in well_founded_tactics in order to solve the size decreasing theorem

Mario Carneiro (May 11 2020 at 09:56):

that needs to be changed to another tactic, and I recommend assumption

Johan Commelin (May 11 2020 at 09:57):

Does that mean a lot of proofs in mathlib will have to be fixed?

Mario Carneiro (May 11 2020 at 09:57):

It does mean a regression for well founded definitions that currently are using the tactic to prove the size decreasing theorem; they will need to put the using_well_founded clause in and reference well_founded_tactic explicitly

Johan Commelin (May 11 2020 at 09:58):

And does lean need to be changed before well_founded_tactics can be removed? You seem to suggest that lean depends on it.

Mario Carneiro (May 11 2020 at 09:58):

Well founded definitions like this are extremely rare in mathlib, and even when they are used the result isn't great, because it does recursion on T.sizeof which has few lemmas

Mario Carneiro (May 11 2020 at 10:03):

well_founded_tactics.default is referenced by lean

Mario Carneiro (May 11 2020 at 10:03):

and it uses default construction of well_founded_tactics, resulting in the use of well_founded_tactics.default_dec_tac

Mario Carneiro (May 11 2020 at 10:04):

So if you change the default value of well_founded_tactics.dec_tac to assumption, you should be able to remove default_dec_tac

Mario Carneiro (May 11 2020 at 10:06):

Another option is to use a def_replacer here, so that users can mark their own default dec_tac, changing the global default

Johan Commelin (May 11 2020 at 10:07):

This sounds orthogonal to norm_num, but maybe not to moving algebra out of core.

Mario Carneiro (May 11 2020 at 10:08):

well_founded_tactics.default_dec_tac is basically a poor man's linarith

Johan Commelin (May 11 2020 at 17:54):

lean#229 is a wip PR that compiles

Johan Commelin (May 11 2020 at 17:55):

I would like some advice on the way forward.

Johan Commelin (May 11 2020 at 17:56):

Previously init.data.nat.lemmas imported init.algebra.functions and hence the entire algebraic hierarchy in core.
Now init.algebra.functions only imports init.algebra.order, and hence init.algebra.{group,field,ordered_ring} etc can all be moved out of core.

Johan Commelin (May 11 2020 at 17:57):

I had to prove something like 20 lemmas specifically for nat and int that would otherwise follow from an ordered_(semi)ring instance.

Kevin Buzzard (May 11 2020 at 17:58):

Wow, so this really is the light at the end of the tunnel?

Johan Commelin (May 11 2020 at 17:58):

Also, nat now has a personal has_dvd instance, and int its own has_sub instance, because they can't get them from comm_semiring resp. add_group.

Kevin Buzzard (May 11 2020 at 17:58):

When you posted that graph earlier I was just thinking that this might be impossible

Kevin Buzzard (May 11 2020 at 17:59):

Nat also has its own has_pow instance though, and this causes lots of problems

Johan Commelin (May 11 2020 at 17:59):

But mine are defeq to what you would get otherwise

Kevin Buzzard (May 11 2020 at 18:00):

I was hoping you'd say that :-)

Johan Commelin (May 11 2020 at 20:37):

So, for lean#229 should I now remove all the init.algebra.* stuff from core? Or should I wait for a bit, so that people can look at what the PR looks like now?

Yury G. Kudryashov (May 11 2020 at 20:52):

For me, it would be easier to look at a version with deleted code (as opposed to commented out or not imported anymore).

Yury G. Kudryashov (May 11 2020 at 20:53):

I wonder what should we do with copyrights when we move code to mathlib, especially when we move code out of files (c) Microsoft to files (c) list of authors.

Patrick Massot (May 11 2020 at 20:55):

It would be more polite to ask Leo about this copyright thing.

Yury G. Kudryashov (May 11 2020 at 21:07):

Who volunteers to ask Leo?

Johan Commelin (May 11 2020 at 21:10):

I've removed the unshackled files, but I haven't yet cleaned up commented out code.

Johan Commelin (May 11 2020 at 21:10):

Going to bed now.

Johan Commelin (May 11 2020 at 21:10):

Others should feel absolutely free to also push to this PR branch

Patrick Massot (May 11 2020 at 21:22):

Yury G. Kudryashov said:

Who volunteers to ask Leo?

I volunteer Kevin. But I think it should be pretty easy to explain. We saw that Lean 4 removed a lot of maths from the core library hence we want to do the same, and we have a technical question about headers.

Kevin Buzzard (May 11 2020 at 22:05):

I can certainly do it

Johan Commelin (May 13 2020 at 06:31):

python3 script/gen_constants_cpp.py src/library/constants.txt
# ------------------------------------------------------
Warning: generated function 'get_le_refl_name' is not used in the source code
Warning: generated function 'get_mul_one_name' is not used in the source code
Warning: generated function 'get_mul_zero_name' is not used in the source code
Warning: generated function 'get_zero_le_one_name' is not used in the source code
Warning: generated function 'get_zero_lt_one_name' is not used in the source code
Warning: generated function 'get_zero_mul_name' is not used in the source code

Johan Commelin (May 13 2020 at 06:31):

lean ./tests/lean/run/check_constants.lean | grep error | sed 's/\/home.*error/error/'
# ------------------------------------------------------
error: identifier 'add_comm_group' is not a constant, namespace nor attribute
error: identifier 'add_comm_semigroup' is not a constant, namespace nor attribute
error: identifier 'add_group' is not a constant, namespace nor attribute
error: identifier 'add_monoid' is not a constant, namespace nor attribute
error: identifier 'distrib' is not a constant, namespace nor attribute
error: identifier 'field' is not a constant, namespace nor attribute
error: identifier 'int.bit0_nonneg' is not a constant, namespace nor attribute
error: identifier 'int.bit0_pos' is not a constant, namespace nor attribute
error: identifier 'int.bit1_nonneg' is not a constant, namespace nor attribute
error: identifier 'int.bit1_pos' is not a constant, namespace nor attribute
error: identifier 'int.nat_abs_bit0_step' is not a constant, namespace nor attribute
error: identifier 'int.nat_abs_bit1_nonneg_step' is not a constant, namespace nor attribute
error: identifier 'int.ne_neg_of_ne' is not a constant, namespace nor attribute
error: identifier 'int.ne_neg_of_pos' is not a constant, namespace nor attribute
error: identifier 'int.ne_of_nat_ne_nonneg_case' is not a constant, namespace nor attribute
error: identifier 'int.neg_ne_of_pos' is not a constant, namespace nor attribute
error: identifier 'int.neg_ne_zero_of_ne' is not a constant, namespace nor attribute
error: identifier 'int.one_nonneg' is not a constant, namespace nor attribute
error: identifier 'int.one_pos' is not a constant, namespace nor attribute
error: identifier 'int.zero_ne_neg_of_ne' is not a constant, namespace nor attribute
error: identifier 'int.zero_nonneg' is not a constant, namespace nor attribute
error: identifier 'left_distrib' is not a constant, namespace nor attribute
error: identifier 'linear_ordered_ring' is not a constant, namespace nor attribute
error: identifier 'linear_ordered_semiring' is not a constant, namespace nor attribute
error: identifier 'monoid' is not a constant, namespace nor attribute
error: identifier 'mul_one' is not a constant, namespace nor attribute
error: identifier 'mul_zero' is not a constant, namespace nor attribute
error: identifier 'mul_zero_class' is not a constant, namespace nor attribute
error: identifier 'right_distrib' is not a constant, namespace nor attribute
error: identifier 'ring' is not a constant, namespace nor attribute
error: identifier 'semiring' is not a constant, namespace nor attribute
error: identifier 'zero_le_one' is not a constant, namespace nor attribute
error: identifier 'zero_lt_one' is not a constant, namespace nor attribute
error: identifier 'zero_mul' is not a constant, namespace nor attribute

Johan Commelin (May 13 2020 at 06:32):

How much of these constants do we really want to keep in core?

Johan Commelin (May 13 2020 at 06:32):

All the int.* stuff should probably stay. But whatever comes after that, I would rather see the end of it.

Johan Commelin (May 13 2020 at 06:33):

We can have nat.left_distrib and int.left_distrib in core, and the general left_distrib in mathlib.

Johan Commelin (May 13 2020 at 08:17):

@Gabriel Ebner @Mario Carneiro Do we want to keep all those constants? I at least want ordered_monoid out of core. Which means that I need to reprove things like neg_of_neg_pos for int if we want to keep all the int.*. How important is that?

Gabriel Ebner (May 13 2020 at 09:09):

I don't see any way to remove the stuff about integers. This is required by the equation compiler to prove that -42 ≠ 358.

Johan Commelin (May 13 2020 at 09:10):

Ok

Johan Commelin (May 13 2020 at 09:10):

I'll reprove the ordered ring stuff for int

Johan Commelin (May 13 2020 at 12:57):

Ok, now the list looks like this

lean ./tests/lean/run/check_constants.lean | grep error | sed 's/\/home.*error/error/'
# -------------------------------------
error: identifier 'add_comm_group' is not a constant, namespace nor attribute
error: identifier 'add_comm_semigroup' is not a constant, namespace nor attribute
error: identifier 'add_group' is not a constant, namespace nor attribute
error: identifier 'add_monoid' is not a constant, namespace nor attribute
error: identifier 'distrib' is not a constant, namespace nor attribute
error: identifier 'field' is not a constant, namespace nor attribute
error: identifier 'left_distrib' is not a constant, namespace nor attribute
error: identifier 'linear_ordered_ring' is not a constant, namespace nor attribute
error: identifier 'linear_ordered_semiring' is not a constant, namespace nor attribute
error: identifier 'monoid' is not a constant, namespace nor attribute
error: identifier 'mul_one' is not a constant, namespace nor attribute
error: identifier 'mul_zero' is not a constant, namespace nor attribute
error: identifier 'mul_zero_class' is not a constant, namespace nor attribute
error: identifier 'right_distrib' is not a constant, namespace nor attribute
error: identifier 'ring' is not a constant, namespace nor attribute
error: identifier 'semiring' is not a constant, namespace nor attribute
error: identifier 'zero_le_one' is not a constant, namespace nor attribute
error: identifier 'zero_lt_one' is not a constant, namespace nor attribute
error: identifier 'zero_mul' is not a constant, namespace nor attribute

Johan Commelin (May 13 2020 at 12:57):

@Gabriel Ebner How do I tell lean that we want to move this out of core?

Gabriel Ebner (May 13 2020 at 12:59):

You've already removed it from constants.txt?

Johan Commelin (May 13 2020 at 13:02):

No, I've not

Johan Commelin (May 13 2020 at 13:02):

I'll rerun the python script

Johan Commelin (May 13 2020 at 13:02):

python3 script/gen_constants_cpp.py src/library/constants.txt
# -----------------------------------
Warning: generated function 'get_le_refl_name' is not used in the source code
Warning: generated function 'get_mul_one_name' is not used in the source code
Warning: generated function 'get_mul_zero_name' is not used in the source code
Warning: generated function 'get_zero_le_one_name' is not used in the source code
Warning: generated function 'get_zero_lt_one_name' is not used in the source code
Warning: generated function 'get_zero_mul_name' is not used in the source code

Johan Commelin (May 13 2020 at 13:02):

Is that bad?

Johan Commelin (May 13 2020 at 13:07):

I've pushed what I have so far

Gabriel Ebner (May 13 2020 at 13:10):

You need to remove more.

Johan Commelin (May 13 2020 at 13:10):

Ok, I should do this manually? Not using some script?

Gabriel Ebner (May 13 2020 at 13:11):

The contents of constants.txt are human-edited.

Johan Commelin (May 13 2020 at 13:17):

Ok, I pushed again

Johan Commelin (May 13 2020 at 13:19):

Errors during make:

/home/jmc/data/math/lean/src/library/app_builder.cpp: In member function ‘lean::expr lean::app_builder::mk_partial_left_distrib(const lean::expr&)’:
/home/jmc/data/math/lean/src/library/app_builder.cpp:742:77: error: ‘get_distrib_name’ was not declared in this scope; did you mean ‘get_string_name’?
  742 |         auto A_distrib = m_ctx.mk_class_instance(::lean::mk_app(mk_constant(get_distrib_name(), {lvl}), A));
      |                                                                             ^~~~~~~~~~~~~~~~
      |                                                                             get_string_name
/home/jmc/data/math/lean/src/library/app_builder.cpp:747:43: error: ‘get_left_distrib_name’ was not declared in this scope; did you mean ‘get_left_comm_name’?
  747 |         return ::lean::mk_app(mk_constant(get_left_distrib_name(), {lvl}), A, *A_distrib);
      |                                           ^~~~~~~~~~~~~~~~~~~~~
      |                                           get_left_comm_name
/home/jmc/data/math/lean/src/library/app_builder.cpp: In member function ‘lean::expr lean::app_builder::mk_partial_right_distrib(const lean::expr&)’:
/home/jmc/data/math/lean/src/library/app_builder.cpp:752:77: error: ‘get_distrib_name’ was not declared in this scope; did you mean ‘get_string_name’?
  752 |         auto A_distrib = m_ctx.mk_class_instance(::lean::mk_app(mk_constant(get_distrib_name(), {lvl}), A));
      |                                                                             ^~~~~~~~~~~~~~~~
      |                                                                             get_string_name
/home/jmc/data/math/lean/src/library/app_builder.cpp:757:43: error: ‘get_right_distrib_name’ was not declared in this scope; did you mean ‘get_iff_intro_name’?
  757 |         return ::lean::mk_app(mk_constant(get_right_distrib_name(), {lvl}), A, *A_distrib);
      |                                           ^~~~~~~~~~~~~~~~~~~~~~
      |                                           get_iff_intro_name

Johan Commelin (May 13 2020 at 13:20):

I'm confused about the internals of lean

Gabriel Ebner (May 13 2020 at 13:25):

Ok, so apparently you removed left_distrib, right_distrib, and distrib even though they're used.

Gabriel Ebner (May 13 2020 at 13:26):

Mmmh, you might want to clean up app_builder.h and app_builder.cpp.

Gabriel Ebner (May 13 2020 at 13:27):

I can also clean up if you're scared.

Johan Commelin (May 13 2020 at 13:38):

@Gabriel Ebner Yes, please go ahead.

Johan Commelin (May 13 2020 at 13:38):

I can help again with fixing the tests.

Johan Commelin (May 13 2020 at 13:38):

But this part, I don't really know what to do.

Gabriel Ebner (May 13 2020 at 13:55):

Done: https://github.com/leanprover-community/lean/pull/229/commits/245b721f98fd11f565dfe8f985cc86381f896e4d

Johan Commelin (May 13 2020 at 13:55):

Thanks!

Johan Commelin (May 13 2020 at 15:34):

:head_bandage: There are 66 failing tests :sad:

Johan Commelin (May 13 2020 at 16:57):

Where do I actually find this test

1 - style_check (Failed)

Gabriel Ebner (May 13 2020 at 16:58):

This is a python script. Apparently I included util.h twice in app_builder.cpp. Just delete the second occurrence.

Johan Commelin (May 13 2020 at 17:10):

What should I do with a test like this

variable R : Type
variable [ring R]

example : -(-(1:R)) = 1 :=
begin
  trace_state,
  exact neg_neg 1,
end

#check - -(1:R)

Yury G. Kudryashov (May 13 2020 at 17:48):

What is it supposed to check?

Johan Commelin (May 13 2020 at 17:49):

https://github.com/leanprover/lean/issues/1862

Johan Commelin (May 13 2020 at 17:49):

There's lots of tests like that.

Johan Commelin (May 13 2020 at 17:49):

They test for a specific bug report.

Yury G. Kudryashov (May 13 2020 at 17:50):

I'd declare a custom class with extends has_neg and an axiom neg_neg.

Kevin Buzzard (May 13 2020 at 17:50):

wooah, I try to prove it with trivial. What even is that?

Johan Commelin (May 13 2020 at 17:52):

Yury G. Kudryashov said:

I'd declare a custom class with extends has_neg and an axiom neg_neg.

I see. That seems like a reasonable approach.

Johan Commelin (May 13 2020 at 19:07):

In case anyone wants to contribute:

        588 - leanruntest_auto_quote1.lean (Failed)
        609 - leanruntest_bin_tree.lean (Failed)
        640 - leanruntest_cc_ac1.lean (Failed)
        641 - leanruntest_cc_ac2.lean (Failed)
        642 - leanruntest_cc_ac3.lean (Failed)
        644 - leanruntest_cc_ac5.lean (Failed)
        645 - leanruntest_cc_ac_bug.lean (Failed)
        687 - leanruntest_conv_tac1.lean (Failed)
        688 - leanruntest_cpdt.lean (Failed)
        742 - leanruntest_dsimp_options.lean (Failed)
        744 - leanruntest_dsimp_proj.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        794 - leanruntest_eq_cases_on.lean (Failed)
        815 - leanruntest_exhaustive_vm_impl_test.lean (Failed)
        830 - leanruntest_funext_tactic.lean (Failed)
        836 - leanruntest_handthen.lean (Failed)
        848 - leanruntest_hinst_lemma1.lean (Failed)
        849 - leanruntest_hinst_lemmas1.lean (Failed)
        892 - leanruntest_interactive1.lean (Failed)
        894 - leanruntest_intros_defeq_canonizer_bug.lean (Failed)
        929 - leanruntest_local_attribute.lean (Failed)
        935 - leanruntest_mario_type_context.lean (Failed)
        977 - leanruntest_mrw.lean (Failed)
        987 - leanruntest_name_resolution_with_params_bug.lean (Failed)
        994 - leanruntest_nat_sub_ematch.lean (Failed)
        1053 - leanruntest_psum_wf_rec.lean (Failed)
        1089 - leanruntest_rw1.lean (Failed)
        1095 - leanruntest_sebastien_coe_simp.lean (Failed)
        1110 - leanruntest_show_goal.lean (Failed)
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
        1128 - leanruntest_simp_lemmas_with_mvars.lean (Failed)
        1139 - leanruntest_simp_tc_err.lean (Failed)
        1142 - leanruntest_simp_zeta.lean (Failed)
        1152 - leanruntest_smt_assert_define.lean (Failed)
        1154 - leanruntest_smt_ematch1.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1157 - leanruntest_smt_ematch_alg_issue.lean (Failed)
        1162 - leanruntest_smt_tests.lean (Failed)
        1211 - leanruntest_term_app2.lean (Failed)
        1224 - leanruntest_u_eq_max_u_v.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)
        1287 - leanittest_goal_info.lean (Failed)

Johan Commelin (May 13 2020 at 19:07):

I just pushed a fix of 10 tests. (Not included on the list above.)

Bryan Gin-ge Chen (May 13 2020 at 19:09):

Looks like your local path snuck into the test output: https://github.com/leanprover-community/lean/pull/229/files#diff-9aa4d9cb8974761857542a0004292d74R1

Johan Commelin (May 13 2020 at 19:15):

Ooh, I though I had fixed that.

Johan Commelin (May 13 2020 at 19:16):

Should be fixed now

Johan Commelin (May 13 2020 at 19:28):

I've broken runtest 1442: https://github.com/leanprover/lean/issues/1442

protected def rel :  ×    ×   Prop
| n₁, d₁ n₂, d₂ := n₁ * d₂ = n₂ * d₁

private def mul' :  ×    ×    × 
| n₁, d₁ n₂, d₂ := n₁ * n₂, d₁ * d₂

example : (a b c d :  × ), rel a c  rel b d  rel (mul' a b) (mul' c d) :=
λ⟨n₁, d₁ n₂, d₂ n₃, d₃ n₄, d₄,
  assume (h₁ : n₁ * d₃ = n₃ * d₁) (h₂ : n₂ * d₄ = n₄ * d₂),
  show (n₁ * n₂) * (d₃ * d₄) = (n₃ * n₄) * (d₁ * d₂),
    by cc

This is specifically about cc, afaict.
What should I do?

Mario Carneiro (May 13 2020 at 19:29):

do you have the proof that * is commutative and associative?

Gabriel Ebner (May 13 2020 at 19:29):

Have you read my comment? I'm pretty sure it's this:

(by cc : a + b = b + a) requires instances for is_associative (+) and is_commutative (+). Add them back (locally?). Same goes for ac_refl.

Johan Commelin (May 13 2020 at 19:31):

Ok, thanks

Johan Commelin (May 13 2020 at 19:53):

Hmm, how should I make this one happy?

universe variables u

-- jmc added this
class ring (α : Type u) extends has_mul α, has_add α :=
(add_comm :  a b : α, a + b = b + a)
(add_assoc :  a b c : α, a + b + c = a + (b + c))

variables {α : Type u}
variables [ring α]
open tactic

-- jmc added this
instance aa : is_associative α (+) := ring.add_assoc
instance ac : is_commutative α (+) := ring.add_comm
constant ma : is_associative α (*)
constant lc : is_left_cancel α (+)
constant rc : is_right_cancel α (+)
constant ld : is_left_distrib α (*) (+)
constant rd : is_right_distrib α (*) (+)

example (x1 x2 x3 x4 x5 x6 : α) : x1*x4 = x1  x3*x6 = x5*x5  x5 = x4  x6 = x2  x1 = x1*(x6*x3) :=
by cc

example (y1 y2 x2 x3 x4 x5 x6 : α) : (y1 + y2)*x4 = (y2 + y1)  x3*x6 = x5*x5  x5 = x4  x6 = x2  (y2 + y1) = (y1 + y2)*(x6*x3) :=
by cc

example (y1 y2 y3 x2 x3 x4 x5 x6 : α) : (y1 + y2)*x4 = (y3 + y1)  x3*x6 = x5*x5  x5 = x4  x6 = x2  y2 = y3  (y2 + y1) = (y1 + y3)*(x6*x3) :=
by cc

Johan Commelin (May 13 2020 at 20:24):

There's a whole bunch of tests using smt and eblast etc. And I have no idea what those are.

Johan Commelin (May 13 2020 at 20:41):

I've pushed what I've done so far. That's it for tonight. I think most of the remaining tests require some help.

Johan Commelin (May 14 2020 at 04:48):

We're now down to 20 failing tests:

        559 - leanruntest_aexp.lean (Failed)
        642 - leanruntest_cc_ac3.lean (Failed)
        644 - leanruntest_cc_ac5.lean (Failed)
        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        815 - leanruntest_exhaustive_vm_impl_test.lean (Failed)
~~        987 - leanruntest_name_resolution_with_params_bug.lean (Failed)~~
        994 - leanruntest_nat_sub_ematch.lean (Failed)
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
~~        1128 - leanruntest_simp_lemmas_with_mvars.lean (Failed)~~
        1152 - leanruntest_smt_assert_define.lean (Failed)
        1154 - leanruntest_smt_ematch1.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1157 - leanruntest_smt_ematch_alg_issue.lean (Failed)
        1162 - leanruntest_smt_tests.lean (Failed)
~~        1211 - leanruntest_term_app2.lean (Failed)~~
~~        1224 - leanruntest_u_eq_max_u_v.lean (Failed)~~
        1247 - leanruntest_using_smt2.lean (Failed)

Johan Commelin (May 14 2020 at 04:59):

Down to 16

Johan Commelin (May 14 2020 at 05:30):

Down to 10

        559 - leanruntest_aexp.lean (Failed)
        644 - leanruntest_cc_ac5.lean (Failed)
        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
~~        815 - leanruntest_exhaustive_vm_impl_test.lean (Failed)~~
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1157 - leanruntest_smt_ematch_alg_issue.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

Johan Commelin (May 14 2020 at 05:32):

I'm removing gcd from core. Is that ok? Or is this something that should strictly stay there for VM reasons?

Mario Carneiro (May 14 2020 at 05:39):

I don't think so. It does seem a bit out of place, come to think of it

Johan Commelin (May 14 2020 at 06:29):

@Mario Carneiro Ok, then I feel good about removing it from the exhaustive_vm_impl_test.

Johan Commelin (May 14 2020 at 06:53):

@Mario Carneiro @Gabriel Ebner Do we want all these smt and eblast tests on ring and field if we are moving those structures out of core? I have no idea what smt and eblast do. I've been able to fix a bunch of tests by changing add_comm to nat.add_comm. But now I'm stuck.

Mario Carneiro (May 14 2020 at 06:54):

You should be able to locally define ring and field in the test(s)

Johan Commelin (May 14 2020 at 06:54):

That's not enough, right?

Johan Commelin (May 14 2020 at 06:54):

You also need a ton of supporting lemmas

Mario Carneiro (May 14 2020 at 06:54):

they work based on attributes like simp does

Mario Carneiro (May 14 2020 at 06:55):

the lemmas don't have to be proven

Johan Commelin (May 14 2020 at 06:55):

That's what I mean

Johan Commelin (May 14 2020 at 06:55):

Aha

Johan Commelin (May 14 2020 at 06:55):

But still. It would mean that these tests become quite a bit longer

Mario Carneiro (May 14 2020 at 06:55):

I guess it depends on the test

Johan Commelin (May 14 2020 at 06:56):

For 56 tests I could do it (-;

Mario Carneiro (May 14 2020 at 06:56):

I mean, is it something that is actually integration testing all these attributes in a library, or is it some particular feature of smt

Johan Commelin (May 14 2020 at 06:57):

I can also dump init/algebra in tests/lean/run/algebra and import stuff.

Johan Commelin (May 14 2020 at 06:57):

Mario Carneiro said:

I mean, is it something that is actually integration testing all these attributes in a library, or is it some particular feature of smt

How would I know?

Johan Commelin (May 14 2020 at 06:57):

These tests are mostly a mystery to me.

Mario Carneiro (May 14 2020 at 06:57):

which one are you looking at now?

Johan Commelin (May 14 2020 at 06:57):

It's code, and if it compiles I'm happy. They mostly don't contain comments explaining what they test.

Johan Commelin (May 14 2020 at 06:58):

Any of

        559 - leanruntest_aexp.lean (Failed)
        644 - leanruntest_cc_ac5.lean (Failed)
        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1157 - leanruntest_smt_ematch_alg_issue.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

Johan Commelin (May 14 2020 at 06:58):

I've fixed all the others

Mario Carneiro (May 14 2020 at 07:00):

aexp.lean doesn't have any algebra in it

Johan Commelin (May 14 2020 at 07:00):

Right... so why is it failing?

Mario Carneiro (May 14 2020 at 07:00):

what errors are you getting? #mwe

Johan Commelin (May 14 2020 at 07:01):

tactic failed, there are unsolved goals
state:
8 goals
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ,
a_3 : asimp_const a_a = val a_2
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 : uname,
a_3 : asimp_const a_a = var a_2
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 a_3 : aexp,
a_4 : asimp_const a_a = plus a_2 a_3
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 a_3 : aexp,
a_4 : asimp_const a_a = times a_2 a_3
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ,
a_3 : asimp_const a_a = val a_2
 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 : uname,
a_3 : asimp_const a_a = var a_2
 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 a_3 : aexp,
a_4 : asimp_const a_a = plus a_2 a_3
 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 a_3 : aexp,
a_4 : asimp_const a_a = times a_2 a_3
 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

Johan Commelin (May 14 2020 at 07:04):

@Mario Carneiro You say that it doesn't have any algebra in it. But it is building expressions with * and +.

Johan Commelin (May 14 2020 at 07:04):

I think it is applying those to nats. And core no longer knows that nat is a comm_semiring. But all the relevant lemmas are there.

Johan Commelin (May 14 2020 at 07:05):

Adding the ematch attribute to nat.zero_mul, nat.zero_add, nat.add_zero, nat.mul_zero didn't help.

Mario Carneiro (May 14 2020 at 07:06):

It's weird; I think the theorem being proven is actually true without any axioms about nat

Mario Carneiro (May 14 2020 at 07:07):

the only thing that should be necessary is that value has + * 0 1

Mario Carneiro (May 14 2020 at 07:07):

I thought it was simplifying 0 + x = x and so on but that's not actually needed

Mario Carneiro (May 14 2020 at 07:07):

but the proof method is really bizarre

Mario Carneiro (May 14 2020 at 07:08):

don't try this at home, kids

Mario Carneiro (May 14 2020 at 07:14):

I just managed to prove the theorem manually using no theorems at all about value

Mario Carneiro (May 14 2020 at 07:17):

What is the state after eblast?

Johan Commelin (May 14 2020 at 07:18):

1 goal
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ,
a_3 : asimp_const a_a = val a_2
facts:
{asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a_2, asimp_const a_a},
 {val a, asimp_const a_a_1},
 {aval a_a s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {aval a_a_1 s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval (asimp_const a_a_1), aval (val a)},
 {a_2 + a, aval (asimp_const (plus a_a a_a_1)) s, aval (val (a_2 + a)) s},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s, aval (plus a_a a_a_1) s}}
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

Mario Carneiro (May 14 2020 at 07:26):

As a quick primer on how to read the state, each of the lists in "equalities" are collections of terms that smt knows how to prove are equal, and the collection as a whole is closed under taking subterms. What was supposed to happen was that since aval a_a s and a_2 are in the same group, and aval a_a_1 s and a are as well, it will deduce that a_2 + a and aval a_a s + aval a_a_1 s are also in the same group, closing the goal. However, they are in different groups. Maybe the typeclass instance on them is different? I suspect that one is addition on nat and the other is addition on value, and the @[reducible] annotation on value is confusing things

Mario Carneiro (May 14 2020 at 07:28):

You could try replacing value with nat everywhere and see if that fixes things

Mario Carneiro (May 14 2020 at 07:28):

although if so this might just be an actual bug

Johan Commelin (May 14 2020 at 07:29):

Mario Carneiro said:

You could try replacing value with nat everywhere and see if that fixes things

Yup, now the error is gone

Mario Carneiro (May 14 2020 at 07:32):

What do the two terms I mentioned look like with pp.all?

Johan Commelin (May 14 2020 at 07:33):

@Mario Carneiro you mean this ¿?

a_ih_a_1 : @eq.{1} nat (imp.aval (imp.asimp_const a_a_1) s) (imp.aval a_a_1 s)
facts:
{@eq.{1} nat (imp.aval (imp.asimp_const a_a_1) s) (imp.aval a_a_1 s),
 @eq.{1} nat (imp.aval (imp.asimp_const a_a) s) (imp.aval a_a s)}
equalities: {{imp.aval a_a s, imp.aval (imp.asimp_const a_a) s}, {imp.aval a_a_1 s, imp.aval (imp.asimp_const a_a_1) s}}

Mario Carneiro (May 14 2020 at 07:34):

after eblast

Johan Commelin (May 14 2020 at 07:34):

How do I print them?

Johan Commelin (May 14 2020 at 07:34):

goals accomplished

Mario Carneiro (May 14 2020 at 07:34):

oh, I mean in the broken version

Mario Carneiro (May 14 2020 at 07:35):

I mean, sure we could change the statement and fix the test, but that kind of defeats the purpose of having a test

Johan Commelin (May 14 2020 at 07:36):

a_3 : @eq.{1} imp.aexp (imp.asimp_const a_a) (imp.aexp.val a_2)
facts:
{@eq.{1} imp.aexp (imp.asimp_const a_a) (imp.aexp.val a_2),
 @eq.{1} imp.aexp (imp.asimp_const a_a_1) (imp.aexp.val a),
 @eq.{1} imp.value (imp.aval (imp.asimp_const a_a_1) s) (imp.aval a_a_1 s),
 @eq.{1} imp.value (imp.aval (imp.asimp_const a_a) s) (imp.aval a_a s)}
equalities:
{{imp.aexp.val a, imp.asimp_const a_a_1},
 {imp.aexp.val a_2, imp.asimp_const a_a},
 {imp.aval a_a s, imp.aval (imp.aexp.val a_2) s, a_2, imp.aval (imp.asimp_const a_a) s},
 {imp.aval (imp.asimp_const a_a), imp.aval (imp.aexp.val a_2)},
 {imp.asimp_const._match_1 (imp.asimp_const a_a), imp.asimp_const._match_1 (imp.aexp.val a_2)},
 {imp.aval a_a_1 s, imp.aval (imp.aexp.val a) s, a, imp.aval (imp.asimp_const a_a_1) s},
 {imp.aval (imp.asimp_const a_a_1), imp.aval (imp.aexp.val a)},
 {imp.aval (imp.asimp_const (imp.aexp.plus a_a a_a_1)),
  imp.aval (imp.aexp.val (@has_add.add.{0} nat nat.has_add a_2 a))},
 {@has_add.add.{0} nat nat.has_add a_2 a,
  imp.aval (imp.asimp_const (imp.aexp.plus a_a a_a_1)) s,
  imp.aval (imp.aexp.val (@has_add.add.{0} nat nat.has_add a_2 a)) s},
 {imp.aexp.val (@has_add.add.{0} nat nat.has_add a_2 a),
  imp.asimp_const (imp.aexp.plus a_a a_a_1),
  imp.asimp_const._match_1 (imp.asimp_const a_a) (imp.asimp_const a_a_1),
  imp.asimp_const._match_1 (imp.aexp.val a_2) (imp.aexp.val a)},
 {@has_add.add.{0} imp.value nat.has_add (imp.aval a_a s) (imp.aval a_a_1 s), imp.aval (imp.aexp.plus a_a a_a_1) s}}

Mario Carneiro (May 14 2020 at 07:36):

@has_add.add.{0} nat nat.has_add a_2 a
@has_add.add.{0} imp.value nat.has_add (imp.aval a_a s) (imp.aval a_a_1 s)

Johan Commelin (May 14 2020 at 07:36):

Mario Carneiro said:

I mean, sure we could change the statement and fix the test, but that kind of defeats the purpose of having a test

Depends on what we're testing, I guess.

Mario Carneiro (May 14 2020 at 07:36):

the adds are indeed different

Johan Commelin (May 14 2020 at 07:39):

So, what do we do now?

Mario Carneiro (May 14 2020 at 07:45):

hm, here's a version of the proof that captures the successful state just before close runs:

lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
begin [smt]
 induction a,
 destruct (asimp_const a_a_1),
{ destruct (asimp_const a_a),
  { ematch, ematch,
    smt_tactic.ematch >> smt_tactic.trace_state },
  all_goals {admit}},
all_goals {admit}
end
equalities:
...
 {@has_add.add.{0} imp.value nat.has_add (imp.aval a_a s) (imp.aval a_a_1 s),
  @has_add.add.{0} nat nat.has_add a_2 a,
  imp.aval (imp.aexp.plus a_a a_a_1) s}}

Johan Commelin (May 14 2020 at 07:45):

I have no idea what that means :oops:

Johan Commelin (May 14 2020 at 07:46):

I feel a bit like I'm a proxy between the master and the machine...

Mario Carneiro (May 14 2020 at 07:47):

I've used smt a grand total of 0 times ever, but I know the theory

Mario Carneiro (May 14 2020 at 07:47):

there is a commented out trace option for smt, what does that show?

Johan Commelin (May 14 2020 at 07:48):

pp.all or not?

Johan Commelin (May 14 2020 at 07:48):

With pp.all you'll get a crapton of shit

Mario Carneiro (May 14 2020 at 07:49):

Use my version of the proof

Mario Carneiro (May 14 2020 at 07:49):

just posted above

Mario Carneiro (May 14 2020 at 07:49):

it stops at the first interesting point

Johan Commelin (May 14 2020 at 07:50):

aexp.lean:65:4: information trace output
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 1
aval (val a_2) s = a_2
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 1
aval (val a) s = a
[smt.ematch] instance [imp.asimp_const.equations._eqn_3], generation: 1
asimp_const (plus a_a a_a_1) = asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1)
[smt.ematch] instance [imp.aval.equations._eqn_3], generation: 1
aval (plus a_a a_a_1) s = aval a_a s + aval a_a_1 s
[smt.ematch] instance, generation: 1, after preprocessing
aval (val a_2) s = a_2
[smt.ematch] instance, generation: 1, after preprocessing
aval (val a) s = a
[smt.ematch] instance, generation: 1, after preprocessing
asimp_const (plus a_a a_a_1) = asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1)
[smt.ematch] instance, generation: 1, after preprocessing
aval (plus a_a a_a_1) s = aval a_a s + aval a_a_1 s

aexp.lean:65:12: information trace output
[smt.ematch] instance [imp.asimp_const._match_1.equations._eqn_1], generation: 2
asimp_const._match_1 (val a_2) (val a) = val (a_2 + a)
[smt.ematch] instance, generation: 2, after preprocessing
asimp_const._match_1 (val a_2) (val a) = val (a_2 + a)

Johan Commelin (May 14 2020 at 07:51):

And

aexp.lean:66:4: information trace output
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 3
aval (val (a_2 + a)) s = a_2 + a
[smt.ematch] instance, generation: 3, after preprocessing
aval (val (a_2 + a)) s = a_2 + a
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ,
a_3 : asimp_const a_a = val a_2
facts:
{asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a, asimp_const a_a_1},
 {val a_2, asimp_const a_a},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval (asimp_const a_a_1), aval (val a)},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval a_a s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {aval a_a_1 s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {a_2 + a, aval (asimp_const (plus a_a a_a_1)) s, aval (val (a_2 + a)) s},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s, aval (plus a_a a_a_1) s}}
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

Mario Carneiro (May 14 2020 at 07:53):

For comparison, here is my version:

aexp.lean:64:4: information trace output
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 1
aval (val a) s = a
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 1
aval (val a_2) s = a_2
[smt.ematch] instance [imp.asimp_const.equations._eqn_3], generation: 1
asimp_const (plus a_a a_a_1) = asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1)
[smt.ematch] instance [imp.aval.equations._eqn_3], generation: 1
aval (plus a_a a_a_1) s = aval a_a s + aval a_a_1 s
[smt.ematch] instance, generation: 1, after preprocessing
aval (val a) s = a
[smt.ematch] instance, generation: 1, after preprocessing
aval (val a_2) s = a_2
[smt.ematch] instance, generation: 1, after preprocessing
asimp_const (plus a_a a_a_1) = asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1)
[smt.ematch] instance, generation: 1, after preprocessing
aval (plus a_a a_a_1) s = aval a_a s + aval a_a_1 s
aexp.lean:64:12: information trace output
[smt.ematch] instance [imp.asimp_const._match_1.equations._eqn_1], generation: 2
asimp_const._match_1 (val a_2) (val a) = val (a_2 + a)
[smt.ematch] instance, generation: 2, after preprocessing
asimp_const._match_1 (val a_2) (val a) = val (a_2 + a)
aexp.lean:65:4: information trace output
[smt.ematch] instance [imp.aval.equations._eqn_1], generation: 3
aval (val (a_2 + a)) s = a_2 + a
[smt.ematch] instance, generation: 3, after preprocessing
aval (val (a_2 + a)) s = a_2 + a
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ,
a_3 : asimp_const a_a = val a_2
facts:
{aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s,
 asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a_2, asimp_const a_a},
 {val a, asimp_const a_a_1},
 {aval a_a_1 s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval a_a s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {aval (asimp_const a_a_1), aval (val a)},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s,
  aval (asimp_const (plus a_a a_a_1)) s,
  aval (val (a_2 + a)) s,
  a_2 + a,
  aval (plus a_a a_a_1) s}}
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

Johan Commelin (May 14 2020 at 07:54):

Am I supposed to solve some problem now? I still have no clue what I'm looking for.

Johan Commelin (May 14 2020 at 07:55):

I think that I would like to learn about SMT, but maybe not while trying to get algebra out of core (-;

Mario Carneiro (May 14 2020 at 07:55):

I'm just diffing

Mario Carneiro (May 14 2020 at 07:58):

I'm ~60% sure you've uncovered a bug in smt, but given that I don't know what we should do about it

Mario Carneiro (May 14 2020 at 07:58):

no one uses it or knows how it works

Johan Commelin (May 14 2020 at 07:59):

And smt is 96% C++, I guess

Mario Carneiro (May 14 2020 at 08:07):

Aha, I think this might be relevant:

lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
begin [smt]
  smt_tactic.get_lemmas >>= smt_tactic.trace,
end
{[imp.asimp_const.equations._eqn_1, patterns: {{asimp_const (val ?x_0)}}],
...
 [imp.asimp_const._match_1.equations._eqn_4, patterns: {{asimp_const._match_1 (val ?x_0) (times ?x_1 ?x_2)}}],
 [one_mul, patterns: {{1 * ?x_2}}],
 [zero_add, patterns: {{0 + ?x_2}}],
 [add_zero, patterns: {{?x_2 + 0}}],
 [imp.aval.equations._eqn_4, patterns: {{aval (times ?x_0 ?x_1) ?x_2}}],
 [mul_one, patterns: {{?x_2 * 1}}],
 [imp.aval.equations._eqn_3, patterns: {{aval (plus ?x_0 ?x_1) ?x_2}}],
 [zero_mul, patterns: {{0 * ?x_2}}],
 [mul_zero, patterns: {{?x_2 * 0}}],
 [nat.add_sub_add_left, patterns: {{?x_0 + ?x_1 - (?x_0 + ?x_2)}}],
 [nat.add_sub_add_right, patterns: {{?x_0 + ?x_1 - (?x_2 + ?x_1)}}],
 [min_eq_right, patterns: {{min ?x_2 ?x_3}}],
 [min_eq_left, patterns: {{min ?x_2 ?x_3}}]}

Mario Carneiro (May 14 2020 at 08:07):

I assume if you run the same thing most of those theorems won't be listed

Mario Carneiro (May 14 2020 at 08:10):

Try adding

attribute [ematch] zero_add add_zero mul_one zero_mul mul_zero
  nat.add_sub_add_left nat.add_sub_add_right min_eq_right min_eq_left

and see if it fixes the issue

Mario Carneiro (May 14 2020 at 08:10):

and then remove lemmas until it breaks again

Johan Commelin (May 14 2020 at 08:25):

@Mario Carneiro I'm back. (Had to put my daughter in bed.) With those attributes, the goal is still

1 goal
s : state,
a_a a_a_1 : aexp,
a_ih_a : aval (asimp_const a_a) s = aval a_a s,
a_ih_a_1 : aval (asimp_const a_a_1) s = aval a_a_1 s,
a : ,
a_1 : asimp_const a_a_1 = val a,
a_2 : ,
a_3 : asimp_const a_a = val a_2
facts:
{asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a_2, asimp_const a_a},
 {val a, asimp_const a_a_1},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval a_a s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval (asimp_const a_a_1), aval (val a)},
 {aval a_a_1 s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {a_2 + a, aval (asimp_const (plus a_a a_a_1)) s, aval (val (a_2 + a)) s},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s, aval (plus a_a a_a_1) s}}
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

just before end.

Mario Carneiro (May 14 2020 at 08:27):

Oh, I missed a couple: nat.add_sub_cancel nat.add_sub_cancel_left

Johan Commelin (May 14 2020 at 08:28):

Too bad, peanut spread...
It's still unhappy.

Mario Carneiro (May 14 2020 at 08:30):

What do you get for this:

attribute [ematch] zero_add add_zero mul_one zero_mul mul_zero
  nat.add_sub_add_left nat.add_sub_add_right min_eq_right min_eq_left
  nat.add_sub_cancel nat.add_sub_cancel_left
lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
begin [smt]
  smt_tactic.get_lemmas >>= smt_tactic.trace,
end
{[imp.asimp_const.equations._eqn_1, patterns: {{asimp_const (val ?x_0)}}],
 [imp.asimp_const.equations._eqn_2, patterns: {{asimp_const (var ?x_0)}}],
 [imp.aval.equations._eqn_1, patterns: {{aval (val ?x_0) ?x_1}}],
 [imp.aval.equations._eqn_2, patterns: {{aval (var ?x_0) ?x_1}}],
 [imp.asimp_const._match_1.equations._eqn_5, patterns: {{asimp_const._match_1 (var ?x_0) ?x_1}}],
 [imp.asimp_const._match_2.equations._eqn_5, patterns: {{asimp_const._match_2 (var ?x_0) ?x_1}}],
 [imp.asimp_const.equations._eqn_3, patterns: {{asimp_const (plus ?x_0 ?x_1)}}],
 [imp.asimp_const.equations._eqn_4, patterns: {{asimp_const (times ?x_0 ?x_1)}}],
 [nat.add_sub_cancel, patterns: {{?x_0 + ?x_1}}],
 [nat.add_sub_cancel, patterns: {{?x_0 + ?x_1 - ?x_1}}],
 [imp.asimp_const._match_2.equations._eqn_2, patterns: {{asimp_const._match_2 (val ?x_0) (var ?x_1)}}],
 [imp.asimp_const._match_1.equations._eqn_2, patterns: {{asimp_const._match_1 (val ?x_0) (var ?x_1)}}],
 [nat.add_sub_cancel_left, patterns: {{?x_0 + ?x_1}}],
 [nat.add_sub_cancel_left, patterns: {{?x_0 + ?x_1 - ?x_0}}],
 [imp.asimp_const._match_2.equations._eqn_6, patterns: {{asimp_const._match_2 (plus ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_2.equations._eqn_7, patterns: {{asimp_const._match_2 (times ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_7, patterns: {{asimp_const._match_1 (times ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_6, patterns: {{asimp_const._match_1 (plus ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_1, patterns: {{asimp_const._match_1 (val ?x_0) (val ?x_1)}}],
 [imp.asimp_const._match_2.equations._eqn_1, patterns: {{asimp_const._match_2 (val ?x_0) (val ?x_1)}}],
 [imp.asimp_const._match_2.equations._eqn_4, patterns: {{asimp_const._match_2 (val ?x_0) (times ?x_1 ?x_2)}}],
 [imp.asimp_const._match_1.equations._eqn_3, patterns: {{asimp_const._match_1 (val ?x_0) (plus ?x_1 ?x_2)}}],
 [imp.asimp_const._match_2.equations._eqn_3, patterns: {{asimp_const._match_2 (val ?x_0) (plus ?x_1 ?x_2)}}],
 [imp.asimp_const._match_1.equations._eqn_4, patterns: {{asimp_const._match_1 (val ?x_0) (times ?x_1 ?x_2)}}],
 [one_mul, patterns: {{1 * ?x_2}}],
 [zero_add, patterns: {{0 + ?x_2}}],
 [add_zero, patterns: {{?x_2 + 0}}],
 [imp.aval.equations._eqn_4, patterns: {{aval (times ?x_0 ?x_1) ?x_2}}],
 [mul_one, patterns: {{?x_2 * 1}}],
 [imp.aval.equations._eqn_3, patterns: {{aval (plus ?x_0 ?x_1) ?x_2}}],
 [zero_mul, patterns: {{0 * ?x_2}}],
 [mul_zero, patterns: {{?x_2 * 0}}],
 [nat.add_sub_add_left, patterns: {{?x_0 + ?x_1 - (?x_0 + ?x_2)}}],
 [nat.add_sub_add_right, patterns: {{?x_0 + ?x_1 - (?x_2 + ?x_1)}}],
 [min_eq_right, patterns: {{min ?x_2 ?x_3}}],
 [min_eq_left, patterns: {{min ?x_2 ?x_3}}]}

Johan Commelin (May 14 2020 at 08:31):

aexp.lean:69:2: information trace output
{[imp.asimp_const.equations._eqn_1, patterns: {{asimp_const (val ?x_0)}}],
 [imp.asimp_const.equations._eqn_2, patterns: {{asimp_const (var ?x_0)}}],
 [imp.aval.equations._eqn_1, patterns: {{aval (val ?x_0) ?x_1}}],
 [imp.aval.equations._eqn_2, patterns: {{aval (var ?x_0) ?x_1}}],
 [nat.mul_one, patterns: {{?x_0 * 1}}],
 [nat.zero_add, patterns: {{0 + ?x_0}}],
 [imp.asimp_const._match_1.equations._eqn_5, patterns: {{asimp_const._match_1 (var ?x_0) ?x_1}}],
 [nat.add_zero, patterns: {{?x_0 + 0}}],
 [nat.one_mul, patterns: {{1 * ?x_0}}],
 [imp.asimp_const._match_2.equations._eqn_5, patterns: {{asimp_const._match_2 (var ?x_0) ?x_1}}],
 [imp.asimp_const.equations._eqn_3, patterns: {{asimp_const (plus ?x_0 ?x_1)}}],
 [imp.asimp_const.equations._eqn_4, patterns: {{asimp_const (times ?x_0 ?x_1)}}],
 [nat.mul_zero, patterns: {{?x_0 * 0}}],
 [nat.add_sub_cancel, patterns: {{?x_0 + ?x_1}}],
 [nat.add_sub_cancel, patterns: {{?x_0 + ?x_1 - ?x_1}}],
 [imp.asimp_const._match_2.equations._eqn_2, patterns: {{asimp_const._match_2 (val ?x_0) (var ?x_1)}}],
 [nat.zero_mul, patterns: {{0 * ?x_0}}],
 [imp.asimp_const._match_1.equations._eqn_2, patterns: {{asimp_const._match_1 (val ?x_0) (var ?x_1)}}],
 [nat.add_sub_cancel_left, patterns: {{?x_0 + ?x_1}}],
 [nat.add_sub_cancel_left, patterns: {{?x_0 + ?x_1 - ?x_0}}],
 [imp.asimp_const._match_2.equations._eqn_6, patterns: {{asimp_const._match_2 (plus ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_2.equations._eqn_7, patterns: {{asimp_const._match_2 (times ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_7, patterns: {{asimp_const._match_1 (times ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_6, patterns: {{asimp_const._match_1 (plus ?x_0 ?x_1) ?x_2}}],
 [imp.asimp_const._match_1.equations._eqn_1, patterns: {{asimp_const._match_1 (val ?x_0) (val ?x_1)}}],
 [imp.asimp_const._match_2.equations._eqn_1, patterns: {{asimp_const._match_2 (val ?x_0) (val ?x_1)}}],
 [imp.asimp_const._match_2.equations._eqn_4, patterns: {{asimp_const._match_2 (val ?x_0) (times ?x_1 ?x_2)}}],
 [imp.asimp_const._match_1.equations._eqn_3, patterns: {{asimp_const._match_1 (val ?x_0) (plus ?x_1 ?x_2)}}],
 [imp.asimp_const._match_2.equations._eqn_3, patterns: {{asimp_const._match_2 (val ?x_0) (plus ?x_1 ?x_2)}}],
 [imp.asimp_const._match_1.equations._eqn_4, patterns: {{asimp_const._match_1 (val ?x_0) (times ?x_1 ?x_2)}}],
 [imp.aval.equations._eqn_4, patterns: {{aval (times ?x_0 ?x_1) ?x_2}}],
 [imp.aval.equations._eqn_3, patterns: {{aval (plus ?x_0 ?x_1) ?x_2}}],
 [nat.add_sub_add_left, patterns: {{?x_0 + ?x_1 - (?x_0 + ?x_2)}}],
 [nat.add_sub_add_right, patterns: {{?x_0 + ?x_1 - (?x_2 + ?x_1)}}],
 [min_eq_right, patterns: {{min ?x_2 ?x_3}}],
 [min_eq_left, patterns: {{min ?x_2 ?x_3}}]}

Mario Carneiro (May 14 2020 at 08:32):

oh, you are using nat.mul_one instead of mul_one et al

Johan Commelin (May 14 2020 at 08:32):

mul_one doesn't exist

Mario Carneiro (May 14 2020 at 08:32):

try replicating mul_one in this file, i.e. define a dummy ring and the lemmas

Mario Carneiro (May 14 2020 at 08:36):

Here's my theory: ematch isn't actually smart enough to realize that @has_add.add nat nat.has_add and @has_add.add value nat.has_add are the same thing, but when it tries to apply one of these typeclass theorems it is forced to unfold value in order to make the second thing typecheck, and then it all works

Johan Commelin (May 14 2020 at 08:39):

Like this:

class semiring (α : Type) extends has_zero α, has_one α, has_add α, has_mul α.

instance foo : semiring  :=
{ zero := 0,
  one := 1,
  add := (+),
  mul := (*) }

section
variables {α : Type} [semiring α] (a : α)

lemma zero_add : (0:α) + a = a := sorry
lemma add_zero : a + 0 = a := sorry
lemma zero_mul : (0:α) * a = 0 := sorry
lemma mul_zero : a * 0 = 0 := sorry
lemma one_mul : (1:α) * a = a := sorry
lemma mul_one : a * 1 = a := sorry

end

Mario Carneiro (May 14 2020 at 08:39):

Mark them all @[ematch], otherwise yes

Johan Commelin (May 14 2020 at 08:40):

attribute [ematch] zero_add add_zero mul_one zero_mul mul_zero
  nat.add_sub_add_left nat.add_sub_add_right min_eq_right min_eq_left
  nat.add_sub_cancel nat.add_sub_cancel_left

lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
begin [smt]
  smt_tactic.get_lemmas >>= smt_tactic.trace,
end
aexp.lean:91:0: error
tactic failed, there are unsolved goals
state:
a : aexp,
s : state
 aval (asimp_const a) s = aval a s

Mario Carneiro (May 14 2020 at 08:40):

you get no output?

Mario Carneiro (May 14 2020 at 08:41):

You should go back to the original test, that was just diagnostics

Johan Commelin (May 14 2020 at 08:42):

a_3 : asimp_const a_a = val a_2
facts:
{asimp_const a_a = val a_2,
 asimp_const a_a_1 = val a,
 aval (asimp_const a_a_1) s = aval a_a_1 s,
 aval (asimp_const a_a) s = aval a_a s}
equalities:
{{val a, asimp_const a_a_1},
 {val a_2, asimp_const a_a},
 {aval (asimp_const a_a), aval (val a_2)},
 {aval (asimp_const a_a_1), aval (val a)},
 {aval a_a s, aval a_a s + aval a_a_1 s - aval a_a_1 s, aval (val a_2) s, a_2, aval (asimp_const a_a) s},
 {asimp_const._match_1 (asimp_const a_a), asimp_const._match_1 (val a_2)},
 {aval a_a_1 s, aval a_a s + aval a_a_1 s - aval a_a s, aval (val a) s, a, aval (asimp_const a_a_1) s},
 {aval (asimp_const (plus a_a a_a_1)), aval (val (a_2 + a))},
 {has_add.add (aval a_a s), has_add.add a_2},
 {val (a_2 + a),
  asimp_const (plus a_a a_a_1),
  asimp_const._match_1 (asimp_const a_a) (asimp_const a_a_1),
  asimp_const._match_1 (val a_2) (val a)},
 {aval a_a s + aval a_a_1 s, aval (asimp_const (plus a_a a_a_1)) s, aval (val (a_2 + a)) s, a_2 + a},
 {aval a_a s + aval a_a_1 s, aval (plus a_a a_a_1) s}}
 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (plus a_a a_a_1)) s = aval (plus a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

 aval (asimp_const (times a_a a_a_1)) s = aval (times a_a a_a_1) s

Mario Carneiro (May 14 2020 at 08:43):

nooo

Mario Carneiro (May 14 2020 at 08:44):

WTH aval a_a s + aval a_a_1 s literally appears in two equality classes

Mario Carneiro (May 14 2020 at 08:44):

it must be the two versions of it

Mario Carneiro (May 14 2020 at 08:46):

Okay, my curiosity is satisfied. Let's just replace value with nat for the PR and maybe file an issue about this for later

Johan Commelin (May 14 2020 at 08:46):

Are you ready for the next test?

Mario Carneiro (May 14 2020 at 08:46):

heh, I hope it's the same story 8 times

Mario Carneiro (May 14 2020 at 08:47):

cc_ac5.lean - is this one not fixed with ac instances for + and * ?

Johan Commelin (May 14 2020 at 08:48):

niverse variables u

class ring (α : Type u) extends has_mul α, has_add α :=
(add_comm :  a b : α, a + b = b + a)
(add_assoc :  a b c : α, a + b + c = a + (b + c))

variables {α : Type u}
variables [ring α]
open tactic

instance aa : is_associative α (+) := ring.add_assoc
instance ac : is_commutative α (+) := ring.add_comm
constant ma : is_associative α (*)
constant lc : is_left_cancel α (+)
constant rc : is_right_cancel α (+)
constant ld : is_left_distrib α (*) (+)
constant rd : is_right_distrib α (*) (+)

example (x1 x2 x3 x4 x5 x6 : α) : x1*x4 = x1  x3*x6 = x5*x5  x5 = x4  x6 = x2  x1 = x1*(x6*x3) :=
by cc

example (y1 y2 x2 x3 x4 x5 x6 : α) : (y1 + y2)*x4 = (y2 + y1)  x3*x6 = x5*x5  x5 = x4  x6 = x2  (y2 + y1) = (y1 + y2)*(x6*x3) :=
by cc

example (y1 y2 y3 x2 x3 x4 x5 x6 : α) : (y1 + y2)*x4 = (y3 + y1)  x3*x6 = x5*x5  x5 = x4  x6 = x2  y2 = y3  (y2 + y1) = (y1 + y3)*(x6*x3) :=
by cc

is what I have so far

Johan Commelin (May 14 2020 at 08:49):

cc fails on all three tests.

Mario Carneiro (May 14 2020 at 08:52):

it's a commutative ring

Johan Commelin (May 14 2020 at 08:53):

Nope it's not. The [ring \a] was from the original test.

Johan Commelin (May 14 2020 at 08:53):

Also, adding commutativity of * doesn't make cc happy.

Mario Carneiro (May 14 2020 at 08:53):

not in my copy

Johan Commelin (May 14 2020 at 08:54):

Oh, weird.

Mario Carneiro (May 14 2020 at 08:56):

If you use

instance ma : is_associative α (*) := sorry
instance mc : is_commutative α (*) := sorry

instead of constant ma : is_associative ... it works

Mario Carneiro (May 14 2020 at 08:56):

I think lean likes to be able to unfold instances to constructors

Johan Commelin (May 14 2020 at 08:56):

Aha

Mario Carneiro (May 14 2020 at 08:56):

even if there isn't anything past that

Mario Carneiro (May 14 2020 at 08:56):

you could use an axiom in place of the sorry

Johan Commelin (May 14 2020 at 08:58):

Ok, thanks. That worked. 2 down, 8 to go.

Johan Commelin (May 14 2020 at 08:58):

leanruntest_cpdt.lean

Mario Carneiro (May 14 2020 at 08:59):

oh boy, rsimp

Mario Carneiro (May 14 2020 at 08:59):

this one uses smt, so it might be the same bug

Mario Carneiro (May 14 2020 at 09:00):

it's also practically the same problem

Mario Carneiro (May 14 2020 at 09:00):

what error do you get?

Johan Commelin (May 14 2020 at 09:01):

/- "Proving in the Large" chapter of CPDT -/

inductive exp : Type
| Const (n : nat) : exp
| Plus (e1 e2 : exp) : exp
| Mult (e1 e2 : exp) : exp

open exp

def eeval : exp  nat
| (Const n)    := n
| (Plus e1 e2) := eeval e1 + eeval e2
| (Mult e1 e2) := eeval e1 * eeval e2

def times (k : nat) : exp  exp
| (Const n)    := Const (k * n)
| (Plus e1 e2) := Plus (times e1) (times e2)
| (Mult e1 e2) := Mult (times e1) e2

def reassoc : exp  exp
| (Const n)    := (Const n)
| (Plus e1 e2) :=
  let e1' := reassoc e1 in
  let e2' := reassoc e2 in
  match e2' with
  | (Plus e21 e22) := Plus (Plus e1' e21) e22
  | _              := Plus e1' e2'
  end
| (Mult e1 e2) :=
  let e1' := reassoc e1 in
  let e2' := reassoc e2 in
  match e2' with
  | (Mult e21 e22) := Mult (Mult e1' e21) e22
  | _              := Mult e1' e2'
  end

@[simp]
lemma nat.mul_left_comm :  (n m k : ), n * (m * k) = m * (n * k) := sorry

attribute [simp] nat.left_distrib nat.right_distrib times reassoc eeval nat.mul_comm nat.mul_assoc

theorem eeval_times (k e) : eeval (times k e) = k * eeval e :=
by induction e; simp [*]

theorem reassoc_correct (e) : eeval (reassoc e) = eeval e :=
by induction e; simp [*]; cases (reassoc e_e2); rsimp

The first one is happy.

Johan Commelin (May 14 2020 at 09:01):

tactic failed, there are unsolved goals
state:
e_e1 e_e2 : exp,
e_ih_e1 : eeval (reassoc e_e1) = eeval e_e1,
e1 e2 : exp,
e_ih_e2 : eeval (Plus e1 e2) = eeval e_e2
 eeval (Plus (Plus (reassoc e_e1) e1) e2) = eeval e_e1 + eeval e_e2

Mario Carneiro (May 14 2020 at 09:01):

you left off mul_left_comm

Johan Commelin (May 14 2020 at 09:02):

It's tagged simp just above

Mario Carneiro (May 14 2020 at 09:02):

oh wait nvm

Johan Commelin (May 14 2020 at 09:15):

ematch_attr_to_defs
------------------------
universe variables u
variable {α : Type u}

def app : list α  list α  list α
| []     l := l
| (h::t) l := h :: app t l

/- Mark the app equational lemmas as ematching rules -/
attribute [ematch] app

@[ematch] lemma app_nil_right (l : list α) : app l [] = l :=
begin [smt]
  induction l,
  ematch,
end

@[ematch] lemma app_assoc (l₁ l₂ l₃ : list α) : app (app l₁ l₂) l₃ = app l₁ (app l₂ l₃) :=
begin [smt]
  induction l₁,
  ematch,
  ematch
end

def len : list α  nat
| []       := 0
| (a :: l) := len l + 1

attribute [ematch] len nat.add_zero nat.zero_add

@[simp] lemma len_app (l₁ l₂ : list α) : len (app l₁ l₂) = len l₁ + len l₂ :=
begin [smt]
  induction l₁,
  {ematch, ematch},
  {ematch, ematch}
end

This one is also confusing me.

Mario Carneiro (May 14 2020 at 09:16):

I think we should just file the ematch based tests away

Mario Carneiro (May 14 2020 at 09:17):

I remember there was some bug in ematch that we found 2 years ago and couldn't do anything about, something to do with multiple typeclasses causing problems for category theory, and we basically banned ematch based proofs from mathlib then

Johan Commelin (May 14 2020 at 09:19):

I managed to fix another test in the mean time

Johan Commelin (May 14 2020 at 09:19):

The list is now

        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1127 - leanruntest_simp_lemma_issue.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

Johan Commelin (May 14 2020 at 09:22):

How about this

universe variables u

class comm_semiring (α : Type*) extends has_zero α, has_add α, has_one α, has_mul α.

lemma zero_add {α : Type*} [comm_semiring α] (a : α) : (0:α) + a = a := sorry
lemma add_zero {α : Type*} [comm_semiring α] (a : α) : a + 0 = a := sorry

def ex {α : Type u} [comm_semiring α] (a : α) : 0 + a = a :=
zero_add a

-- local attribute [-simp] zero_add add_zero
attribute [simp] ex

example (a b : nat) : 0 + 0 + a = a :=
by simp -- !!! FAILS :shock:

-- local attribute [-ematch] zero_add add_zero
attribute [ematch] ex

example (a b : nat) : 0 + 0 + a = a :=
by using_smt $ smt_tactic.eblast -- fails :not_surprised:

Johan Commelin (May 14 2020 at 09:23):

Ooh, nvm... nat is not a comm_semiring

Johan Commelin (May 14 2020 at 09:23):

That one's fixed.

Johan Commelin (May 14 2020 at 09:27):

        688 - leanruntest_cpdt.lean (Failed)
        767 - leanruntest_ematch2.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

Mario Carneiro (May 14 2020 at 09:31):

is cpdt fixed with a fake ring instance?

Mario Carneiro (May 14 2020 at 09:32):

from the names it looks like everything that remains is ematch related, so let's just comment out these tests

Mario Carneiro (May 14 2020 at 09:35):

Is ematch2.lean not fixed with a fake instance?

Johan Commelin (May 14 2020 at 09:37):

The last blast in ematch2:

tactic failed, there are unsolved goals
state:
α : Type u,
p m n q : ,
xs : tuple α m,
ys : tuple α n,
zs : tuple α p,
ws : tuple α q,
a : p = n + m,
a_1 : zs == xs ++ ys
 zs ++ ws == xs ++ (ys ++ ws)

Mario Carneiro (May 14 2020 at 09:40):

I think it needs add_assoc on nat

Mario Carneiro (May 14 2020 at 09:41):

try attribute [ematch] nat.add_assoc

Mario Carneiro (May 14 2020 at 09:42):

oh crap, I just realized the implications of the @[no_rsimp] attribute

Johan Commelin (May 14 2020 at 09:44):

From the end of cpdt:

class semiring (α : Type) extends has_mul α, has_add α, has_one α, has_zero α.

instance foo : semiring nat :=
{ zero := 0, one := 1, add := (+), mul := (*) }

variables {α : Type} [semiring α] (a b c : α)

lemma left_distrib : a * (b + c) = a * b + a * c := sorry
lemma right_distrib : (a + b) * c = a * c + b * c := sorry
lemma mul_comm : a * b = b * a := sorry
lemma mul_assoc : a * b * c = a * (b * c) := sorry
lemma mul_left_comm : a * (b * c) = b * (a * c) := sorry

attribute [simp] left_distrib right_distrib times reassoc eeval mul_comm mul_assoc mul_left_comm

theorem eeval_times (k e) : eeval (times k e) = k * eeval e :=
by induction e; simp [*]

theorem reassoc_correct (e) : eeval (reassoc e) = eeval e :=
by induction e; simp [*]; cases (reassoc e_e2); rsimp -- still fails

Johan Commelin (May 14 2020 at 09:44):

Mario Carneiro said:

try attribute [ematch] nat.add_assoc

This didn't help.

Mario Carneiro (May 14 2020 at 09:47):

What do you get in cpdt with set_option trace.smt true?

Mario Carneiro (May 14 2020 at 09:47):

I think the second block is the first one that fails

Johan Commelin (May 14 2020 at 09:53):

test ematch2 is now fixed. smt_ematch2 is still a problem.
Let me look at cpdt again.

Johan Commelin (May 14 2020 at 09:54):

 Freeze display
Tactic State
1 goal
e : exp
 eeval (reassoc e) = eeval e
cpdt.lean:58:3: error
tactic failed, there are unsolved goals
state:
e_e1 e_e2 : exp,
e_ih_e1 : eeval (reassoc e_e1) = eeval e_e1,
e1 e2 : exp,
e_ih_e2 : eeval (Plus e1 e2) = eeval e_e2
 eeval (Plus (Plus (reassoc e_e1) e1) e2) = eeval e_e1 + eeval e_e2
cpdt.lean:58:48: information trace output
[smt.intro] e_e1 : exp
[smt.intro] e_e2 : exp
[smt.fact] new facts: {eeval (reassoc e_e1) = eeval e_e1}
[smt.intro] e_ih_e1 : eeval (reassoc e_e1) = eeval e_e1
[smt.intro] n : 
[smt.fact] new facts: {eeval (Const n) = eeval e_e2}
[smt.intro] e_ih_e2 : eeval (Const n) = eeval e_e2
[smt.ematch] new ground fact: bnot ff = tt
[smt.ematch] new ground fact: bnot tt = ff
[smt.ematch] new ground fact: bxor ff tt = tt
[smt.ematch] new ground fact: bxor tt ff = tt
[smt.ematch] new ground fact: ff || tt = tt
[smt.ematch] new ground fact: bxor ff ff = ff
[smt.ematch] new ground fact: 0 = 0
[smt.ematch] new ground fact: tt && ff = ff
[smt.ematch] new ground fact: ff || ff = ff
[smt.ematch] new ground fact: tt && tt = tt
[smt.ematch] new ground fact: bxor tt tt = ff
[smt.ematch] new ground fact: nat.bodd 1 = tt
[smt.ematch] new ground fact: nat.bodd 0 = ff
[smt.ematch] new ground fact: ff = false
[smt.fact] new facts: {ff}
[smt.ematch] new ground fact: tt = true
[smt.fact] new facts: {tt}
[smt.ematch] new ground fact: int.sign 1 = 1
[smt.ematch] new ground fact: int.sign 0 = 0
[smt.ematch] new ground fact: nat.pred 0 = 0
[smt.ematch] new ground fact: nat.div2 0 = 0
[smt.ematch] new ground fact: nat.div2 1 = 0
[smt.ematch] new ground fact: nat.bodd 2 = ff
[smt.ematch] new ground fact: nat.bit ff 0 = 0
[smt.ematch] new ground fact: nat.div2 2 = 1
[smt.ematch] new ground fact: tt = true
[smt.fact] new facts: {tt}
[smt.ematch] new ground fact: ff = false
[smt.fact] new facts: {ff}
[smt.ematch] new ground fact: int.sign (-1) = -1
[smt.ematch] instance [bor_self], generation: 1
ff || ff = ff
[smt.ematch] instance [band_self], generation: 1
tt && tt = tt
[smt.ematch] instance [bxor_ff], generation: 1
bxor ff ff = ff
[smt.ematch] instance [bxor_ff], generation: 1
bxor tt ff = tt
[smt.ematch] instance [bnot_bnot], generation: 1
bnot (bnot tt) = tt
[smt.ematch] instance [bnot_bnot], generation: 1
bnot (bnot ff) = ff
[smt.ematch] instance [bor_ff], generation: 1
ff || ff = ff
[smt.ematch] instance [eeval.equations._eqn_1], generation: 1
eeval (Const n) = n
[smt.ematch] instance [tt_band], generation: 1
tt && ff = ff
[smt.ematch] instance [tt_band], generation: 1
tt && tt = tt
[smt.ematch] instance [ff_bxor], generation: 1
bxor ff ff = ff
[smt.ematch] instance [ff_bxor], generation: 1
bxor ff tt = tt
[smt.ematch] instance [ff_bor], generation: 1
ff || ff = ff
[smt.ematch] instance [ff_bor], generation: 1
ff || tt = tt
[smt.ematch] instance [band_tt], generation: 1
tt && tt = tt
[smt.ematch] instance [bxor_self], generation: 1
bxor ff ff = ff
[smt.ematch] instance [bxor_self], generation: 1
bxor tt tt = ff
[smt.ematch] instance [band_ff], generation: 1
tt && ff = ff
[smt.ematch] instance [bor_tt], generation: 1
ff || tt = tt
[smt.ematch] instance [tt_bxor], generation: 1
bxor tt tt = bnot tt
[smt.ematch] instance [tt_bxor], generation: 1
bxor tt ff = bnot ff
[smt.ematch] instance [bxor_tt], generation: 1
bxor tt tt = bnot tt
[smt.ematch] instance [bxor_tt], generation: 1
bxor ff tt = bnot ff
[smt.ematch] instance [reassoc._match_1.equations._eqn_1], generation: 1
reassoc._match_1 (reassoc e_e1) (Const n) (Const n) = Plus (reassoc e_e1) (Const n)
[smt.ematch] instance [bnot_eq_true_eq_eq_ff], generation: 1
bnot ff = tt = (ff = ff)
[smt.ematch] instance [bnot_eq_ff_eq_eq_tt], generation: 1
bnot tt = ff = (tt = tt)
[smt.ematch] instance [bxor_coe_iff], generation: 1
(bxor ff ff)  xor ff ff
[smt.ematch] instance [bxor_coe_iff], generation: 1
(bxor tt tt)  xor tt tt
[smt.ematch] instance [bxor_coe_iff], generation: 1
(bxor ff tt)  xor ff tt
[smt.ematch] instance [bxor_coe_iff], generation: 1
(bxor tt ff)  xor tt ff
[smt.ematch] instance [band_coe_iff], generation: 1
(tt && ff)  tt  ff
[smt.ematch] instance [band_coe_iff], generation: 1
(tt && tt)  tt  tt
[smt.ematch] instance [bor_coe_iff], generation: 1
(ff || ff)  ff  ff
[smt.ematch] instance [bor_coe_iff], generation: 1
(ff || tt)  ff  tt
[smt.ematch] instance [band_eq_true_eq_eq_tt_and_eq_tt], generation: 1
tt && tt = tt = (tt = tt  tt = tt)
[smt.ematch] instance [band_eq_false_eq_eq_ff_or_eq_ff], generation: 1
tt && ff = ff = (tt = ff  ff = ff)
[smt.ematch] instance [bor_eq_true_eq_eq_tt_or_eq_tt], generation: 1
ff || tt = tt = (ff = tt  tt = tt)
[smt.ematch] instance [bor_eq_false_eq_eq_ff_and_eq_ff], generation: 1
ff || ff = ff = (ff = ff  ff = ff)
[smt.ematch] instance, generation: 1, after preprocessing
ff || ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
tt && tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt ff = tt
[smt.ematch] instance, generation: 1, after preprocessing
bnot (bnot tt) = tt
[smt.ematch] instance, generation: 1, after preprocessing
bnot (bnot ff) = ff
[smt.ematch] instance, generation: 1, after preprocessing
ff || ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
eeval (Const n) = n
[smt.ematch] instance, generation: 1, after preprocessing
tt && ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
tt && tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
ff || ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
ff || tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
tt && tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt tt = ff
[smt.ematch] instance, generation: 1, after preprocessing
tt && ff = ff
[smt.ematch] instance, generation: 1, after preprocessing
ff || tt = tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt tt = bnot tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt ff = bnot ff
[smt.ematch] instance, generation: 1, after preprocessing
bxor tt tt = bnot tt
[smt.ematch] instance, generation: 1, after preprocessing
bxor ff tt = bnot ff
[smt.ematch] instance, generation: 1, after preprocessing
reassoc._match_1 (reassoc e_e1) (Const n) (Const n) = Plus (reassoc e_e1) (Const n)
[smt.ematch] instance, generation: 1, after preprocessing
bnot ff = tt = (ff = ff)
[smt.fact] new facts: {ff = ff, bnot ff = tt}
[smt.ematch] instance, generation: 1, after preprocessing
bnot tt = ff = (tt = tt)
[smt.fact] new facts: {tt = tt, bnot tt = ff}
[smt.ematch] instance, generation: 1, after preprocessing
(bxor ff ff)  xor ff ff
[smt.fact] new facts: {(bxor ff ff), xor ff ff}
[smt.ematch] instance, generation: 1, after preprocessing
(bxor tt tt)  xor tt tt
[smt.fact] new facts: {(bxor tt tt), xor tt tt}
[smt.ematch] instance, generation: 1, after preprocessing
(bxor ff tt)  xor ff tt
[smt.fact] new facts: {(bxor ff tt), xor ff tt}
[smt.ematch] instance, generation: 1, after preprocessing
(bxor tt ff)  xor tt ff
[smt.fact] new facts: {(bxor tt ff), xor tt ff}
[smt.ematch] instance, generation: 1, after preprocessing
(tt && ff)  tt  ff
[smt.fact] new facts: {tt  ff, (tt && ff)}
[smt.ematch] instance, generation: 1, after preprocessing
(tt && tt)  tt  tt
[smt.fact] new facts: {tt  tt, (tt && tt)}
[smt.ematch] instance, generation: 1, after preprocessing
(ff || ff)  ff  ff
[smt.fact] new facts: {ff  ff, (ff || ff)}
[smt.ematch] instance, generation: 1, after preprocessing
(ff || tt)  ff  tt
[smt.fact] new facts: {ff  tt, (ff || tt)}
[smt.ematch] instance, generation: 1, after preprocessing
tt && tt = tt = (tt = tt  tt = tt)
[smt.fact] new facts: {tt = tt  tt = tt, tt && tt = tt}
[smt.ematch] instance, generation: 1, after preprocessing
tt && ff = ff = (false  ff = ff)
[smt.fact] new facts: {false  ff = ff, tt && ff = ff}
[smt.ematch] instance, generation: 1, after preprocessing
ff || tt = tt = (false  tt = tt)
[smt.fact] new facts: {false  tt = tt, ff || tt = tt}
[smt.ematch] instance, generation: 1, after preprocessing
ff || ff = ff = (ff = ff  ff = ff)
[smt.fact] new facts: {ff = ff  ff = ff, ff || ff = ff}
[smt.ematch] instance [eeval.equations._eqn_2], generation: 2
eeval (Plus (reassoc e_e1) (Const n)) = eeval (reassoc e_e1) + eeval (Const n)
[smt.ematch] instance, generation: 2, after preprocessing
eeval (Plus (reassoc e_e1) (Const n)) = eeval (reassoc e_e1) + eeval (Const n)
[smt.fact] new facts: {eeval (reassoc._match_1 (reassoc e_e1) (Const n) (Const n)) = eeval e_e1 + eeval e_e2}
cpdt.lean:58:48: information trace output
[smt.intro] e_e1 : exp
[smt.intro] e_e2 : exp
[smt.fact] new facts: {eeval (reassoc e_e1) = eeval e_e1}
[smt.intro] e_ih_e1 : eeval (reassoc e_e1) = eeval e_e1
[smt.intro] e1 : exp
[smt.intro] e2 : exp
[smt.fact] new facts: {eeval (Plus e1 e2) = eeval e_e2}
[smt.intro] e_ih_e2 : eeval (Plus e1 e2) = eeval e_e2
[smt.ematch] new ground fact: bnot ff = tt
[smt.ematch] new ground fact: bnot tt = ff
[smt.ematch] new ground fact: bxor ff tt = tt
[smt.ematch] new ground fact: bxor tt ff = tt
[smt.ematch] new ground fact: ff || tt = tt
[smt.ematch] new ground fact: bxor ff ff = ff
[smt.ematch] new ground fact: 0 = 0
[smt.ematch] new ground fact: tt && ff = ff
[smt.ematch] new ground fact: ff || ff = ff
[smt.ematch] new ground fact: tt && tt = tt
[smt.ematch] new ground fact: bxor tt tt = ff
[smt.ematch] new ground fact: nat.bodd 1 = tt
[smt.ematch] new ground fact: nat.bodd 0 = ff
[smt.ematch] new ground fact: ff = false
[smt.fact] new facts: {ff}
[smt.ematch] new ground fact: tt = true
[smt.fact] new f

Johan Commelin (May 14 2020 at 09:56):

@Gabriel Ebner How do you feel about commenting out the remaining tests?

Johan Commelin (May 14 2020 at 09:59):

We are talking about

99% tests passed, 5 tests failed out of 1359

Total Test time (real) = 169.26 sec

The following tests FAILED:
        688 - leanruntest_cpdt.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)
        1247 - leanruntest_using_smt2.lean (Failed)

Gabriel Ebner (May 14 2020 at 10:10):

Yeah, ematching tests -> remove

Gabriel Ebner (May 14 2020 at 10:10):

cpdt -> remove

Gabriel Ebner (May 14 2020 at 10:11):

using_smt2 -> is everything broken? That would be bad. If it's just two examples or so -> remove the examples.

Johan Commelin (May 14 2020 at 10:37):

Ok, I'll do that

Johan Commelin (May 14 2020 at 10:44):

Done and pushed.
But locally it still says

The following tests FAILED:
        688 - leanruntest_cpdt.lean (Failed)
        768 - leanruntest_ematch_attr_to_defs.lean (Failed)
        1155 - leanruntest_smt_ematch2.lean (Failed)
        1156 - leanruntest_smt_ematch3.lean (Failed)

even though I removed those tests from tests/lean/run/*

Gabriel Ebner (May 14 2020 at 10:46):

Locally? You need to re-run cmake.

Johan Commelin (May 14 2020 at 10:48):

Aha

Johan Commelin (May 14 2020 at 10:48):

I've pushed... this PR is now touching 106 files :shock:

Gabriel Ebner (May 14 2020 at 10:50):

To come back to your question from the other thread: should we make a release before we merge this PR?

Johan Commelin (May 14 2020 at 10:53):

I think it makes sense. I certainly don't feel brave enough to fix mathlib after the 6 different PR that we now have in core...

Johan Commelin (May 14 2020 at 10:53):

I prefer to take small steps. But I don't have a good overview.

Johan Commelin (May 14 2020 at 10:53):

This has very much been a cargo cult PR from my side

Gabriel Ebner (May 14 2020 at 10:57):

There's still one failing test. I'll then get 3.12 out of the door today, and we can think about 3.13 tomorrow.

Johan Commelin (May 14 2020 at 10:59):

Yes, I just noticed the failing test. It should be fixed now.

Johan Commelin (May 14 2020 at 11:21):

Hooray! Locally it builds without errors and all the (remaining) tests pass!


Last updated: Dec 20 2023 at 11:08 UTC