[isabelle-dev] isabelle dimacs2hol
makarius at sketis.net
Thu Aug 1 16:41:18 CEST 2013
On Wed, 10 Jul 2013, Tjark Weber wrote:
>> I vaguely remember a private discussion about the performance of inner
>> syntax parsing in this respect. For a realistic import one would
>> bypass that anyway, i.e. not generate source files to parse them again,
>> but read things directly via some Isabelle/ML functions.
> Agreed. Related functionality is available in HOL/ex/SAT_Examples.thy.
(Cleaning up old mail threads ...)
Looking superficially at
I wonder if this actually works right now.
It used to be subject to "try use_thy ..." for several years, and the
current HOL/ROOT has it commented-out.
If you have some ambition to put it into shape, I can give some hints what
needs to be done. E.g. global ML reference variables need to be
eliminated and replaced by "configuration options" in ML (structure Config
with certain operations in structure Attrib) or "system options" in
ML/Scala (which are subject to persistent user preferences, potentially
available in the front-end).
More information about the isabelle-dev