Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)



On Mon, 17 Sep 2012, Rafal Kolanski wrote:

I don't know how else to explain this, other than that the Isabelle users list is great, helpful and proving stuff is fun and easy to release, working at the ML level is a depressing experience, and trying to share the results of one's work doubly so.

This has already become a running gag: someone, maybe even Gerwin, decided at some point that Isabelle has an "Isar level for users" and an "ML level for developers". But I've myself never introduced anything like that.

The very first Isar command I implemented in the distant past was 'ML'. And today Isabelle/Isar and Isabelle/ML are neatly intertwined such that you can go back and forth between the languages as you need in your tool implementations. The Prover IDE is also a fairly good IDE for ML inside regular Isar source.

So you have Isabelle/Pure/HOL/ML/Isar/Scala etc but it is difficult to assign "levels" to them. In practice you work with several of these Isabelle aspects at the same time. The delicate bootstrapping process in the Isabelle/Pure implementation is a different story -- the machine room down there is definitely not user-space.


	Makarius





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