Re: [isabelle] Slots for diagnostic value command



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

On 31/07/14 09:48, Florian Haftmann wrote:
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:
* Slot »default« implementents the current behavior and is the default.
* The former slots (s.a.) are restored again.

Any comments?

This is something I definitely do not promote for the approaching
release, but rather for its successor.

	Florian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.