Re: [isabelle] I need an ML function to get the THY path and filename



On 14-04-02 17:40, Gottfried Barrow wrote:
That's the idea I'm pursuing.

It gets back to filtering to figure out what the good ideas are.

I know I need ML to get a more powerful and faster version of "value", to export code, import code, and then do some tests, part of which might involve calling Perl for data processing. I want to keep it all internal to a THY because I don't define HOL functions to export them and do any programming with them. Functions are just a means to get to the next function, which may someday lead to a function which would be good to export and do some programming with.

As to scripts, continuous proving doesn't work for build scripts, so that's where the console comes in to run programs, ML being one of the options for programming. So I set my environment to here:

/cygdrive/e/E_2/dev/Isabelle2013-2/contrib/polyml-5.5.1-1/x86-cygwin/poly.exe

I haven't even tried using that directly yet, because it all can take a lot of experimentation, but there's also the SML/NJ that I have installed.

I say all that to say that if I'm running ML directly, then I guess I'm back to using OS.Process.system to call Perl. All that takes time to figure out, especially where I'm at in all this.

Thanks,
GB




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