when compiling Poly/ML is configure
--without-x (libXm dependencies are really fragile).
The last time I say the X11/Motif interface being used was the first
version of "XIsabelle" in 1996.
Makarius
___
polyml mailing list
polyml@in
gual plane", such as
blackbord-bold B.
Recently we have introduced one minor change to this encoding-agnostic
approach in Isabelle: 1 line of ML to count character positions, which
ignores anything from the range of 128..192. This fits well with UTF-8
and als
I am working with named pipes to output large amounts of text to an
external process. Looking at the sources of basis/TextIO.sml etc. I've
got the impression that pipes are always line-buffered. Is there an easy
way to get block-buffering?
Mak
uch an image.
This homegrown variant of "fat binaries" works quite well across a broad
range of platforms, e.g. see the 7 platforms available via
http://isabelle.in.tum.de/download_x86-linux.html
Only in rare situations, some users with very old Linux installations ev
? (Right now
there is only a single open/unassigned item on the tracker by myself.)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
runtime configuration (setting global flags), and that is intentionally
not undoable.
Frequently ".ML" in upper case is used for ML source although case isn't
significant on Windows. ".sml" is also widely used.
Isabelle/ML always uses .ML
lot of existing code around.
In Isabelle/ML we now more or less assume that there are no chdirs and no
side effects on refs. We are lucky enough to can afford this in our
specific framework, which provides its own ways to manage context data
without side effects.
Makarius
_
might confuse people who don't like spaces. E.g. in
foo::@{thms bar}
the "::@" part is taken as a single ML name. Infixes are better
surrounded by spaces anyway, e.g.
foo :: @{thms bar}
(This discussion is better continued on t
Maybe the following paper is of some interest to Poly/ML users:
Makarius Wenzel. Parallel Proof Checking in Isabelle/Isar. In G. Dos
Reis and L. Théry, editors. The ACM SIGSAM 2009 International Workshop
on Programming Languages for Mechanized Mathematics Systems. Munich,
August 2009. To
reaches its natural performance end with approx. 4 cores. Running
Isabelle on 16 cores typically requires 16-32 GB memory, and 64bit is then
the only way.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman
Err of raised
Using plain ":" instead of ":>" above will produce "" in both
cases.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
ature/functor layer in ML.
Interestingly, opaque signature matching also causes problems in SML/NJ
pretty printing. I consider to make another attempt at abstype within a
non-opaque structure, trying to avoid the nested structure within the
abstract type.
Mak
On Wed, 16 Sep 2009, Makarius wrote:
On Wed, 16 Sep 2009, David Matthews wrote:
To be honest, when I think of an abstract type I think of the abstype
construction rather than opaque signature matching.
Interestingly, opaque signature matching also causes problems in SML/NJ
pretty printing
The following paper might be interesting to users of ML who care about
performance on current multicore hardware.
David C. J. Matthews and Makarius Wenzel. Efficient Parallel Programming
in Poly/ML and Isabelle/ML. Proceedings of the ACM SIGPLAN Workshop on
Declarative Aspects of
ignificant improvements in the new
scheme. E.g. we can pass additional properties through the pp output,
without affecting indentation produced by Poly/ML. This allows to pass
our own position information and additional markup, which will become
particularly important in the coming post-tty inte
= Task_Queue.new_group NONE;
val x = Future.fork_group g loop;
val y = Future.fork_group g (fn () => 1 div 0);
The library implementation is fine-tuned towards the particular needs of
Isabelle proof checking, but it should be straight forward to turn this
into a fully gene
On Fri, 12 Feb 2010, Makarius wrote:
$ Isabelle2009-1/bin/isabelle tty -l HOL
Welcome to Isabelle/HOL (Isabelle2009-1: December 2009)
> exit
ML>
And invoke it as above, replacing "HOL" by "Pure" in the command line.
BTW, in this tty mode the nominal n
I've run into the same problem on Mac OS (Snow Leopard), compiling for
x86-darwin or x86_64-darwin.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
, greater than the
usual line length. This produces funny output with
PolyML.print/makestring, because it does not do the formatting as observed
above.
Is it possible to force breaks more directly, apart from embedding a
literal "\n" which is not counted properly?
ng as a line break.
If you really want to augment the functionality here, I would prefer a
separate PrettyLineBreak constructor.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
econds 3) system "notepad.exe";
Exception- TimeOut raised
Here is another example:
ML> val x = Future.fork (fn () => system "notepad.exe");
ML> Future.cancel x;
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
ehow intrinsic to the way the Poly/ML runtime system
invokes external processes. David can explain that better. (I wonder if
the builtin delay loop is still required these days.)
Makarius
fun elapsed_time f x =
let
val now = Time.now ();
val res = f x;
val _ = TextIO
On Thu, 13 May 2010, David Matthews wrote:
Makarius wrote:
On Linux on the same hardware class the result is like that:
ML> elapsed_time (fn () => join (fork "true")) ();
0.102
These 100ms are somehow intrinsic to the way the Poly/ML runtime system
invokes external proce
Tests for several months already -- updating from the repository
occasionally. My impression is that it is pretty close to stable-release
quality.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
ootFunction;
TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\");
PolyML.SaveState.saveState \"$OUTFILE\"; true);
You can also experiment doing only part of the above.
Makarius
___
polyml mailing list
polyml@inf.ed.
when trying to print Foo (1, "a") for example.
The same kind of code does work with a single type parameter, e.g. for
datatype 'a bar = Bar of 'a
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Mon, 23 Aug 2010, Makarius wrote:
This crashes the RTS when trying to print Foo (1, "a") for example.
Just for the record: this is SVN version 1193.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.
than before, since I can embedd my own
markup into the pretty trees processed by Poly/ML, for example.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Sun, 14 Nov 2010, Rob Arthan wrote:
For the record, you can also achieve this kind of effect with
Posix.IO.dup2. See below for sample code.
This looks like an interesting trick. Can it also handle output produced
by the Poly/ML runtime system (exception_trace etc.)?
Makarius
.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Wed, 16 Feb 2011, Lucas Dixon wrote:
Does anyone know of some HTTP code written in ML? I'd like to
programmatically, in ML, do some web-queries...
There is some in Isabelle2011/src/Tools/WWW_Find/, but that's a server not
a client.
a
has been used in his code base much longer than in Isabelle.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
erning parallel exception handling in this library.)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_SOURCES="$ML_HOME/../src"
You then need to build Pure for that platform:
Isabelle2011/build Pure
or on Mac OS X:
Isabelle2011.app/Isabelle/build Pure
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Tue, 21 Jun 2011, Makarius wrote:
On Tue, 21 Jun 2011, Aleks Kissinger wrote:
On a related note, any idea why Par_List.exists would raise the
"EXCEPTIONS []" exception? The predicate function shouldn't be throwing
exceptions (at least it doesn't with List.exists
On Wed, 5 Oct 2011, Hong Feng wrote:
another question: any way to support the GNU readline library under the SML
system for user interaction?
I am using "rlwrap" for this, it is a separate executable.
Makarius
___
polyml ma
es.
I've occasionally asked myself about the future of the Cygwin platform for
Isabelle users, and was starting to think of MinGW 64 instead.
Fortunately, the Cygwin maintainers have recently woke up, and made some
initial moves towards proper x86_64 support.
here http://www4.in.tum.de/~wenzelm/test/polyml-5.4.1.tar.gz
in the usual Isabelle way. In particular it includes the important
libsha1 binary module, which is otherwise easy to miss.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
rsion 1379 successfully on my usual build platforms,
using the builtin libffi sources: Linux, Mac OS Leopart, Mac OS Snow
Leopard, Cygwin, both with x86/x86_64 in various combinations. Our
libsha1 module also works as expected.
Makarius
able to explain this
better.)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
eak SML/NJ or old versions of Poly/ML
(5.2.1, 5.3.0, 5.4.x). On the other hand it will make testing of old
Isabelle versions with brand new Poly/ML versions more difficult.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
NJ is loosing the game long before 100 MB total heap size,
resulting in a factor 10..100 performance loss due to memory menagement,
compared to Poly/ML.
I've also seen the JVM getting awkward at 1..2 GB heap size.
Makarius
___
polyml ma
/HOL-Library.png (The
scale in these charts is in minites, and the application is heavy-duty
symbolic theorem proving.)
So almost every effort to include Poly/ML in your portfolio will pay off.
Makarius
___
polyml mailing list
polyml
n and
maintenance. Too much activity in proposing new language features means an
extra burden on the rare people who are still there to keep the
implementations going.
David Matthews made huge steps forward in the past few years, without ever
touching the SML'97 standard as such.
py
user of old abstype with old non-opaque signature matching in recent
years.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
andedly by David
Matthews, there a multi-billion dollar company with thousands of
developers. Let's see what Oracle does next to catch up ... :-)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
dd-ons that are now standard.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Wed, 26 Sep 2012, David Matthews wrote:
Makarius sent me a script to do this so he may be able to shed a bit
more light on it but this is what I managed to find.
Here is a dynamic reference to the Isabelle-way of building Poly/ML. The
"tip" will change whenever there is an upd
On Tue, 25 Sep 2012, Mark Wright wrote:
Did you include the important libsha1.so that is
part of the regular Isabelle2012 distribution of Poly/ML?
No, thanks for letting me know I should, I guess I should
build it from the source code here:
https://bitbucket.org/makarius
This is one of the
On Wed, 26 Sep 2012, Bernard Berthomieu wrote:
On 9/26/12 3:35 PM, Makarius wrote:
My current build script for Poly/ML 5.5.0 is this
http://isabelle.in.tum.de/repos/isabelle/file/11bcea724b2c/Admin/polyml/build
Nice ! I might borrow your script :-)
You are welcome.
One detail worth
://isabelle.in.tum.de/repos/isabelle/file/8b20be429cf3/src/Pure/System/system_channel.ML
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
/repos/isabelle/file/Isabelle2012/src/HOL/Library/RBT.thy
You can backport that to SML manually, or use the Isabelle/HOL generator
to produce SML, Haskell, Scala etc. -- the result would not look much
worse than the C -> SML translation performed by hand in SML/NJ some years
a
. Better use Linux here.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
ence for mailing list vs. social network here.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
xcited about how OCaml compilation works.)
One could do a little bit here by including certain polyml options or
shell scripts by default, to address both the scripting and the
batch-compilation problem in a way that looks familiar to the masses.
Makarius
___
"the man in the street" wants to see, though, is something that looks
and feels like "polymlc ..." just like "cc ...", although that might sound
a bit silly.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.
he idea. It is mostly about trivialities for people who know
Poly/ML sufficiently well.
Note that the majority of people out there are not even sceptics of
Poly/ML, because they have not even heard of it. Instead they are using
much worse systems that they are used to.
Makarius
that show
that the extra time for Mlton compilation is worth waiting? (Real
applications, not just micro-benchmarks.)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Tue, 2 Apr 2013, David Matthews wrote:
--skip-first-line option: Skip the first line of the input stream. Used with
scripts with #! at the start.
You should probably insist in an actual "#!" before skipping the first
line, just as a sanity check.
.
* Lack of support for multicore systems.
Any benchmark these days should include parallel processing routinely, but
we should be glad to have support for multicore hardware at all for a few
surviving implementations of Standard ML. (OCaml is really in a pitch
there -- mayb
umption is that future dependencies
are relatively sparse.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
figure --disable-shared",
which I did not know before.
Makarius#!/usr/bin/env bash
#
# Minimal Poly/ML startup script
THIS="$(cd "$(dirname "$0")"; pwd)"
export LD_LIBRARY_PATH="$THIS:$LD_LIBRARY_PATH"
e
hread" of the future task farm.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
question is for the isabelle-users mailing list.
Depending on your Linux distribution, there should be packages for "32" or
"multilib" versions of that basic shared libraries for C and C++ (you need
both).
Makarius
___
polyml
so you don't have to rush anything here.
I am on vacation from 17-Oct-2013 to 04-Nov-2013, which means I will be
unavailable for the usual tests with Isabelle and AFP on all reachable
platforms.
Makarius
___
polyml mailing
Isabelle/jEdit, the Documentation panel on the right-hand side gives quick
access to Examples, notably src/HOL/ex/ML.thy for some Isabelle/ML basics.
The manual on Isabelle/jEdit in the same panel provides further details on
the IDE, which is based on the jEdit text editor.
Makarius
belle/file/Isabelle2013-2/src/Pure/ML-Systems/multithreading_polyml.ML#l177
This involves some overhead to create a fresh item, but later comparisons
are pure, and there is also a conical time-stamp order on it.
Makarius
___
polyml mailing l
re/ML/ml_compiler_polyml.ML#l184
In both cases, the critical bit is the two-stage invocation of
PolyML.compiler: first the static then the dynamic phase.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/lis
On Mon, 3 Mar 2014, Makarius wrote:
(1) short version (Isabelle/Pure bootstrap):
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML-Systems/compiler_polyml.ML#l40
(2) long version (full Isabelle/ML managed compilation with IDE markup)
http://isabelle.in.tum.de
implemented in the past
few years. Cygwin x86_64 has emerged recently, but I have not tried it
yet.
What might be also interesting is MinGW for x86 or x86_64, but I have
not really tried that either.
Makarius
___
polyml mailing list
polyml
-only
world, or imitate Unix-style command-line tinkering directly in the Cygwin
shell.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Mon, 19 May 2014, David Matthews wrote:
Using Cygwin might be a possibility if you are thinking of providing a
separate GUI. The package that Makarius has provided for running
Isabelle on Windows uses Poly/ML under Cygwin but all the user
interaction is through jEdit.
Isabelle/jEdit is
Poly/ML build/run options wrong, such that
statistics are enabled accidentally.
I am also using PolyML.Statistics.getLocalStats, but shouldn't the
shared-memory file be for global stats only?
Makarius
___
polyml mailing list
p
ome enthusiasts of Poly/ML and Isabelle/PIDE can
help to vote up my (updated) answer on the SML IDE in Isabelle2014.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
al references to very
basic things are sometimes surprising, by construction of the initial
environment.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
port to pick useful add-ons from the
Isabelle/ML environment and use them in SML, as well. See also
$ISABELLE_HOME/src/Tools/SML/Examples.thy
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
dy
deleted for the next release. (Such a nostalgic REPL is actually more
complicated than having a direct editing model that is now standard in
Isabelle/PIDE.)
Makarius
http://stop-ttip.org 99
nel, and then edit without
further thinking about it.
An open problem is to generate a compiled application directly from this
IDE model, but right now Isabelle/SML is not a specific "product" for such
standalone application development yet (unless you want to ship
On Thu, 11 Dec 2014, Peter Gammie wrote:
On 11 Dec 2014, at 4:14, Makarius wrote:
I don’t "hack" on Isabelle/Pure, but edit it carefully and
thoughtfully, using plain jEdit with its static ML mode.
Sounds like I might as well use emacs rather than “plain jEdit with its
stat
Qt4 recently, see
https://www.youtube.com/watch?v=ON0A1dsQOV0
Makarius
http://stop-ttip.org
a start, I am considering to make a stand-alone Isabelle/SML/PIDE
distribution next time. I have already reduced the disk footprint
drastically, by using only JRE and not full JDK, and without the
Isabelle/HOL image it will come out rather small.
Makarius
--
/isabellepide-as-ide-for-standard-ml
for a quick start.
Makarius
http://stop-ttip.org 1,145,058 people so far
that still makes some sense
is GTK.
Makarius
http://stop-ttip.org 1,145,216 people so far
ere is mainly a cultural difference: git users like flashy tools and big
noisy communities, Mercurial users like to use a tool quietely without
much ado about it. So strictly speaking, as a Mercurial user I could not
even advertize that here, but on 01-Apr one could probably make an
exception.
also
http://git-man-page-generator.lokaltog.net/
Maybe I shall take a serious look at the Mercurial + Git front-end
https://www.sourcetreeapp.com/ but it would mean to stop using Linux just
for the sake of Git.
Makarius
___
polyml mailing
What is also interesting in this preview of the next Poly/ML release is
native support for x86-windows, based on MingW32 instead of Cygwin.
Cygwin remains the portable system glue for the Isabelle environment, but
both the IDE front-end (Scala/JVM) and the ML backend are now fully at
home on Win
Poly/ML is always x86-windows.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Wed, 26 Aug 2015, Artella Coding wrote:
I tried the msys instructions and encountered an error upon running
"make".
/bin/sh: line 9: makeinfo: command not found
You need to install the texinfo package, e.g. like this:
pacman -S texinfo
On Mon, 7 Sep 2015, David Matthews wrote:
The experimental code is in the Windows-Unicode branch and requires
./configure CPPFLAGS="-DUNICODE -D_UNICODE"
to build the Unicode version. The resulting poly takes a --codepage option
to set the code-page to be used for conversion. Probably "utf8" i
olyml/build
The above polyml/build script may be taken as a blueprint for anybody who
wants to compile it by himself. See also the other files in that
directory, especially INSTALL-MinGW.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
complete SML implementation, based on the existing Poly compiler.
Glad to see that this very first SML project still defines the cutting
edge until today!
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman
the physical file-system. The IDE could also create
required but missing resources on the spot.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
E_HOME, so it can be derefenced dynamically at run-time.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
the process to catch up with all that for the coming winter
release of Isabelle.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
e benefit of the formal markup of the document outline and
pseudo-markup for the text content is that it is managed by Isabelle and
the IDE.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
with local ML bindings, and evaluate ML expressions in a particular
run-time context.
More explanations with a screenshot on
http://sketis.net/2016/ml-debugging-within-the-prover-ide
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http
, but is important: big Isabelle
applications need small 32bit model to avoid requiring the double amount
of heap space.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
ell-checking, but here it is a bit more.
I looked at some online videos but they didnt really help. So how do I
compile and run the src/Tools/SML/Examples.thy file?
You need the active prover session for that, i.e. a startup build that
works.
Makarius
_
ll working towards that
point of text. The Theories panel helps to keep an overview.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
tion and by some
experiments.
I don't think that non-continuous mode is very relevant for actual
debugging. It is more important when composing large ML modules, while
still thinking about the problem and not checking anything yet.
Makarius
1 - 100 of 162 matches
Mail list logo
