Re: [isabelle] A course based on Isabelle/HOL and some feedback...

Le 26/04/12 17:21, Makarius a écrit :
This is one of these scoping errors that then lead to a conflict with
the type constraints imposed by already defined entities, and are thus
discovered indirectly. The type checking phase could be a bit more
ambitious to maintain precise position information and report that
(which is technically not so easy and might require one or two more
release cycles to materialize).

aouch... it sounds that it is unlikely to be present in Isabelle/HOL for next january, the next time I will give the lecture :-)

But the actual scoping is already represented quite nicely in current
Isabelle2011-1 right now, if you use Isabelle/jEdit and rely in its
"Haribo effect". This means the sources are painted in funny colors
according to the role of identifiers. The Prover IDE also has the magic
CONTROL (or COMMAND) key, which asks the system to explain the formal
status of some piece of source.

So the above "id" would have come out black (constant) instead of the
expected blue (free variable), and its tooltip would have said "constant", with a hyperlink to jump to its definition in main HOL. So
students would have to spend less energy divinating the meaning of the
text themselves.

Ok I'll try this... In fact, I was nearly ready to use jEdit for the labs but I found that jEdit was often getting stuck when using nitpick and quickcheck, and since my labs strongly rely on those two tools it was a problem.

However, I am convinced that students would love switching to jEdit because they are really not comfortable with emacs :-)

Best regards,


Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at

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