Email Gateway (Aug 19 2022 at 15:12): Email Gateway (Aug 19 2022 at 15:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
In 4044a7d1720f, there was a change: the ancient »slots« for value
(code, nbe, simp) and the default behaviour of sequential trys have been
given up in favour of one hard-coded behaviour:
If the term to evaluate does not contain free variables, evaluate
using ML.
If the term contains free variables or the first step fails, evaluate
using nbe.
Recent experience suggests that this step was maybe too rigorous since
»value« is also used for purposes beyond diagnostic evaluation which
demand a more predictable behaviour, esp. wrt. ongoing developments of
theories.
My suggestion would be to revive the »slots« as follows:
Any comments?
This is something I definitely do not promote for the approaching
release, but rather for its successor.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:12):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
I'd be in favour of re-introducing the slots. Among others, I have used "value [code]" to
automatically check the sanity of the code generator setup like a regession test.
Andreas
Last updated: Apr 25 2024 at 20:15 UTC