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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and