[isabelle-dev] isabelle dimacs2hol

[Makarius]

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 
http://isabelle.in.tum.de/repos/isabelle/file/b7a83845bc93/src/HOL/ex/SAT_Examples.thy 
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).


 	Makarius