Isabelle-HoTT icon indicating copy to clipboard operation
Isabelle-HoTT copied to clipboard

Published 20 hours ago • verified publisher icon jaycech3n

Tactics looping on Isabelle2021

Open jaycech3n opened this issue 4 years ago • 1 comments

Certain tactics loop on Isabelle2021-RC3. Needs further investigation.

jaycech3n avatar Jan 26 '21 13:01 jaycech3n

Looks like this comes from changes to the substitution tactics in Isabelle2021. See

  • https://isabelle.in.tum.de/dist/Isabelle2021/doc/NEWS.html on "proof method subst", as well as
  • $ISABELE_HOME/src/Tools/eqsubst.ML).

This results in altered computation behavior of the typechecker and simplification methods in I/HoTT. The proofs can be manually patched for now; really we'll want a rewrite of the simplification code at some point.

jaycech3n avatar Apr 17 '21 16:04 jaycech3n