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



On Wed, 2 Apr 2014, Gottfried Barrow wrote:

On 14-04-01 14:04, Makarius wrote:
 Of course, unpredictable or really bad things will happen, when you
 modify the file system in any of these bash commands.

Thanks for the heads up, a casual comment that belies the real message, "WARNING! YOU MAY DESTROY YOUR FILE SYSTEM, FOOL!"

The point here is that the Isar 'bash' command was declared as "diag", so it runs asynchronously and in parallel as far as possible. If you combine this with mutations on the file-system or other global system state, you can easily get some fireworks.

This is also the reason why some insiders of parallel programming say "mutable state is the root of all evil". In the multicore era you are either stateless and fast, or stateful and slow. Some decades ago that was the opposite.

Maybe for your continued experiments, it is better to make 'bash' a "thy_decl" command, to force it into sequential mode (for the current theory file).


I ran the ideas through this filter: "Does any of this give me something over and above what I already have, like Windows Explorer for file management?"

No. One would have to make more substantial reforms of stateless operating systems to fit it into the PIDE model and get real benefits from it. (Apple's Time Machine and the ZFS file-system are actually moving a bit in that direction.)


I attach a THY, along with the one you sent me, to be complete. I make my requests in the THY, and there are 8 comment headings which give an overview of what each section does.

I've looked through this briefly. Note that the double-quoted strings of Parse.name can be avoided by using Parse.text: that category also allows "verbatim" tokens of form {* ... *}.

That brings us back to the pending reform to allow nestable text cartouches in that spot ...


	Makarius




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