Email Gateway (Aug 19 2022 at 13:56): Email Gateway (Aug 19 2022 at 13:56):From: Gottfried Barrow <igbi@gmx.com>
Hi,
I describe what I need, and then I get more verbose about ML and the
PIDE, and recent NEWS.
The export_code command in a THY will create a file in the directory of
the THY. For example, a command like this:
export_code id in SML file "sml_test_output.ML
What ML command do I use to obtain the path and filename of the THY in
which I have ML{...} commands? I did some searches in the src folder
looking for how export_code does that, but all I saw was noise.
This would be part of my very recent attempt to switch to Isabelle/ML as
my primary general purpose programming language. Further, it's part of
my occasional attempt to eliminate some complexity and pursue the goal
of working in "one document, in one language, in one development
environment".
It's not completely achievable, but because ML is a subset of the
languages that can be used with Isar commands, then it does partially
fit the one language goal, and it fits even more the working in only one
IDE.
The availability of ML libraries is quite thin, but there are no
problems, there are only workarounds. In pursuit of regular expressions,
a decent or even better solution might be awk, which I can call from ML,
like this:
ML{*
fun gawkfprint str file = OS.Process.system (
"gawk \"BEGIN { print \\\"" ^ str ^ "\\\" }\" > " ^ file);
gawkfprint "this is a tester4" "test.txt"
*}
Workarounds abound. ML{* OS.Process.system "ls -l" *} only prints the
return code in the output panel. Maybe that's all it's supposed to do.
I include some links.
Regards,
GB
[isabelle-dev] NEWS: Isabelle support for Standard ML
http://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-March/005125.html
http://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-March/005132.html
http://isabelle.in.tum.de/repos/isabelle/file/bea2196627cb/src/Tools/SML
Manual that used to be a book: Gawk: Effective AWK Programming
http://www.gnu.org/software/gawk/manual/
Email Gateway (Aug 19 2022 at 13:57):From: Makarius <makarius@sketis.net>
On Mon, 31 Mar 2014, Gottfried Barrow wrote:
On 14-03-31 11:18, Gottfried Barrow wrote:
export_code id in SML file "sml_test_output.ML"
What ML command do I use to obtain the path and filename of the THY in
which I have ML{...} commands?I'll simplify it. I need the path to the folder that the "sml_test_output.ML"
file is in, which will be the path of my THY, though it would be nice to get
the THY file name also.
The file-system location of a theory is called "master directory": all of
its file-references should be relative to that (although some very old
tools sometimes do it differently).
This is how to access the master directory in an ad-hoc example:
ML {* Thy_Load.master_directory @{theory} *}
This is how to get the formal name of the theory, which is conceptually
different from the file name, but you can reconstruct it yourself:
ML {* Context.theory_name @{theory} *}
Note that @{theory} refers to the compile-time theory context of each ML
snipped. In regular Isabelle/ML programming you pass this around as some
value thy: theory, and feed-in some compile-time constant only where you
invoke it in the end.
Generally, the master directory is still being used, but somewhat
old-fashioned and about to be discontinued: the Prover IDE will eventually
take care of all external resources, and the prover will be devoid of
file-system access.
You have surely noticed already that export_code does not fit 100% into
the picture of continuous theory and proof checking while you type: it
leaves a dirty trace of file-name prefixes in your directory. At some
point in the future, export_code would write into an "abstract file-space"
of the document model, which is committed only when the IDE says so, e.g.
on shutdown.
This probably also means, it is a bad idea to try writing one file here
and reading the same file elsewhere -- that simulates stateful programming
via files, but statefulness is out.
The basic idea is to export code, and right below it, use the exported
code to do some calculations in a ML{...} command.
You can probably avoid all these complications with files, of you use the
generated ML code directly, e.g. via the @{code} antiquotation of
Isabelle/ML.
It is also possible to pass around ML sources as strings or tokens in
Isabelle/ML, and invoke the compiler on it. That is a normal benefit of
incremental compilation.
Doing that, and using ML as a tool for Isabelle in general, and
processing a THY to get some LaTeX are my only programming needs. It's
either learn ML and Perl (not awk), or learn Scala.
Isabelle/ML is for hardcore logic-based tools. Isabelle/Scala is for
higher-order functional-object-oriented systems programming. In that
respect Scala is closer to Perl, e.g. it also supports nice pattern
matching with regexps.
Makarius
Email Gateway (Aug 19 2022 at 13:57):From: Makarius <makarius@sketis.net>
On Mon, 31 Mar 2014, Gottfried Barrow wrote:
The availability of ML libraries is quite thin
There is indeed very little, apart from what you have already on-board in
Isabelle, but that is quite a lot.
but there are no problems, there are only workarounds. In pursuit of
regular expressions, a decent or even better solution might be awk,
which I can call from ML, like this:ML{*
fun gawkfprint str file = OS.Process.system (
"gawk \"BEGIN { print \\\"" ^ str ^ "\\\" }\" > " ^ file);
gawkfprint "this is a tester4" "test.txt"
*}Workarounds abound. ML{* OS.Process.system "ls -l" *} only prints the return
code in the output panel. Maybe that's all it's supposed to do.
OS.Process.system is one of these SML Basis Library functions that should
not be used inside Isabelle, because they don't comply to the Isabelle
system programming model.
Use Isabelle_System.bash or Isabelle_System.bash_output instead.
(Isabelle/Scala provides similar operations.)
[isabelle-dev] NEWS: Isabelle support for Standard ML
http: //mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-March/005125.html
http: //mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-March/005132.html
Anybody who is interested in that is welcome to join on isabelle-dev, but
without cross-posting chaos on isabelle-users.
Makarius
Email Gateway (Aug 19 2022 at 14:07):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 14:15):From: Makarius <makarius@sketis.net>
On Mon, 31 Mar 2014, Gottfried Barrow wrote:
The key word is "internal". When the PIDE is powered up, the goal is to stay
working internal to a THY and the related THY and ML files, as much as
possible. I click on a cntl-hover link to get me files.
Indeed.
I access Unix essentials in the THY, viewing results in the output
panel, not having to resort to the Console, which will allow me to
create a history of commands.
I attach a screenshot and THY to show I'm one, small step closer to the
end result.
I don't know what the end result will be, but here is my contribution to
the game: Bash.thy with CD, PWD, and bash commands inside the theory
context. Note that I could not use the names "cd" and "pwd", since these
are left-over commands from ancient times.
The global working directory of a process (e.g. File.cd) is incompatible
with the idea of stateless execution. By putting the cd value into the
formal context, you can feed that to each shell process individually, and
they can run in parallel unencumbered. This is done by the PIDE
automatically, since the 'bash' command is diagnostic and thus mean to be
without any effects.
Of course, unpredictable or really bad things will happen, when you modify
the file system in any of these bash commands.
Makarius
Bash.thy
Last updated: Apr 20 2024 at 08:16 UTC