Zulip Chat Archive

Stream: general

Topic: master branch is broken


view this post on Zulip Scott Morrison (Oct 07 2018 at 06:07):

Ugh, master is broken in mathlib.

view this post on Zulip Scott Morrison (Oct 07 2018 at 06:07):

arguta:mathlib scott$ git status
On branch master
Your branch is up-to-date with 'origin/master'.

nothing to commit, working tree clean
arguta:mathlib scott$ lean --make tests/tactics.lean
/Users/scott/projects/lean/mathlib/tests/tactics.lean:641:2: error: is_def_eq tactic failed, the following expressions are not definitionally equal (remark: is_def_eq tactic does modify the metavariable assignment)
  p : Prop
and
  s : Prop
state:
p q r s : Prop,
h₀ : p ↔ q,
h₁ : q ↔ r,
h₂ : r ↔ s
⊢ p ↔ s

view this post on Zulip Scott Morrison (Oct 07 2018 at 06:07):

(I spent 20 minutes trying to work out how my branch had broken something, before realising it wasn't my fault.)

view this post on Zulip Simon Hudon (Oct 07 2018 at 06:08):

My bad. we should comment out those tests while I'm fixing that tactic

view this post on Zulip Simon Hudon (Oct 07 2018 at 06:14):

@Mario Carneiro Can you comment out these test cases please?

view this post on Zulip Mario Carneiro (Oct 07 2018 at 06:15):

eh, can you PR it? It takes me an hour to move to and from module branch

view this post on Zulip Simon Hudon (Oct 07 2018 at 06:22):

Here you go: https://github.com/leanprover/mathlib/pull/398


Last updated: May 17 2021 at 23:14 UTC