lt
from the document. This model won't work as expected, if you cause effects on
the surrounding physical world (like writing files).
The proper language for physics (not mathematics) in the Isabelle universe is
Isabelle/Scala: it has a Console window, but is not covere
on the stack.
This is really great.
I have now started to make some tests with Isabelle + AFP, and will come back
eventually with reports (and potential problems).
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http
questions/9555790/does-sml-poly-have-a-cl-like-repl
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
function is first run and should do what you
> want. Give it a try and see how it is.
I am using that in https://isabelle-dev.sketis.net/rISABELLEfca4d6abebda and
it looks fine.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
ersion will leak C memory if the
> build functions are repeatedly called. This was the case before the recent
> changes on the X86 as well. It isn't any longer because the conversion
> functions on the X86 can be garbage collected.
This means we need to get this conceptually right, and cann
he ML heap image can
be portable over processes and OS installations.
That is just my feedback for now. I guess we won't need the division of
compiletime/runtime in Isabelle, because the only Foreign call is SHA1.digest,
used on a few big blobs, and not invoked too often.
Makarius
___
Error
"""
(See also
https://isabelle.sketis.net/repos/isabelle/file/9e5862223442/Admin/polyml/INSTALL-MinGW)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
abelle release will probably be in Jan-2021.)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 07/07/2020 08:41, David Matthews wrote:
> Thanks for producing this example. I've investigated it and the current
> master ( fb10196 ) includes a fix.
>
> The current master should have proper fixes for both the bugs.
> Makarius: Could you check that you don't g
think would
> be useful but they can always be changed. The web site is at
> https://www.polyml.org/software/index.php and is linked from the main Poly/ML
> website at www.polyml.org.
>
> Let me know what you think.
I have registered as "makarius" and tried to add the Isabelle
at gcc generally becomes better over time)
(3) bump c++ standard, leave gcc unchanged: potential loss of
stability (old gcc on new language standard -- unproven technology)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.e
See also this reply on
the old thread:
http://lists.inf.ed.ac.uk/pipermail/polyml/2017-December/002139.html
I am all for bumping up that old MinGW build environment, but it is up
to David Matthews to do something about it, or leave the status-quo
unchanged.
On 19/05/2019 05:57, Matthew Fernandez wrote:
>
> Some time ago I proposed PolyML switch to building with the C++11 standard
> [0]. The main blocking issue that surfaced was Isabelle supporting Ubuntu
> 12.04 which ships without a C++11-enlightened compiler. In January 2019,
>
is again not open source.
Have you tried this (relatively recent) project?
https://chocolatey.org
The package manager for Windows
Chocolatey - Software Management Automation
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http:/
in.tum.de/repos/isabelle/file/9c634887be9e/Admin/bash_process/bash_process.c
So while Poly/ML is running as native Windows application, the
surrounding system environment is that of Cygwin (shell etc.).
Makarius
___
polyml mailing list
polyml@in
ssumes that failed attempts at a
remote connection (e.g. network file-system or socket) do not block
indefinitely, but cause a timeout eventually.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
/Admin/build_polyml.scala
(with specific options for x86-windows and x86_64-windows)
I wonder if it would be better to use the free community version of
Visual Studio instead: https://www.visualstudio.com/downloads
Has anybody tried this and can report some experience with it?
Makarius
On 10/02/18 21:47, Makarius wrote:
> On 10/02/18 21:16, Matthew Fernandez wrote:
>>
>> If I understand your aim correctly, you are trying to alter the path the
>> runtime linker will use to find libpolyml.so. Is it not simpler to
>> statically link to libpolyml inste
needs to be bundled with Poly/ML.
The starting point for the current reorganization was actually a
conflict of the bundled libgmp vs. the system-installed libgmp, see
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2018-February/
p for x86_64-darwin).
See also the full story in
http://isabelle.in.tum.de/repos/isabelle/file/4fb9cbe10f3e/Admin/polyml/README#l26
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
t assumes that libgmp has been installed in a standard place
(e.g. /usr/local/lib).
I wonder if anybody has managed to build libgmp for x86-darwin (32bit)
platform. That platform variant still provides better performance for
big applications like Isabelle, because it requires only half the memory.
stall
chrpath -r '$ORIGIN/../lib' target/bin/poly
Here is a proof for the result:
ldd target/bin/poly
linux-vdso.so.1 => (0x7fffdc799000)
libpolyml.so.9 =>
/home/makarius/lib/polyml/polyml-git/target/bin/../lib/libpolyml.so.9
(0x7f4b02d98000)
libc.so.6 => /lib/x
ot; next to "-lgmp" above does not work, probably
because these options also apply to the build process of libpolyml itself.
How can I make libpolyml a static part of poly?
Alternatively, how can I make libgcc and libstdc++ a static part of
libpolyml?
Makarius
__
On 18/12/17 03:07, Matthew Fernandez wrote:
>
>> On Dec 16, 2017, at 03:24, Makarius <makar...@sketis.net
>> <mailto:makar...@sketis.net>> wrote:
>>
>> For Isabelle the situation is documented here:
>> http://isabelle.in.tum.de/repos/isabelle/file/tip/
OS X
10.10) and use it on a newer one? Is there any chance to do this with
x86 instead of x86_64?
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
the newer Foreign interface already 13 months ago: the
following change may serve as example how to do it:
http://isabelle.in.tum.de/repos/isabelle/rev/4fb8560df827
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.u
On 25/11/17 22:45, Makarius wrote:
> On 25/11/17 18:44, David Matthews wrote:
>
>> I've had a better look and I found that I was seeing this as well. I've
>> pushed a fix and it no longer seems to be doing it. It's a very small
>> change so I would be very surprised i
Ubuntu 12.04 LTS test systems.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
effect is somewhat non-deterministic, but it appears quite reliably
on my reference machines for x86-linux and x86_64-linux (Ubuntu 12.04 LTS).
In most other system configurations it appears to work.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
n at the end of the week.
I have successfully built this version on Linux, Windows, mac OS, and
ran vorious manual tests of Isabelle + AFP. It all looks fine.
Note that I will be on travel on Wed--Fri this week, so if there are any
last-minute issues, I cannot do any tests during these days.
le.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/index.html#session_Iptables_Semantics_Examples_Big
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
s/Iptables_Semantics_Examples_Big_heap_chart.png
Here are the overall results:
timing:
1:47:37 elapsed time, 8:17:10 cpu time, factor 4.62
ML timing:
1:47:33 elapsed time, 10:16:19 cpu time, factor 5.73
maximum heap:
29997 M
average heap:
25795 M
Isabelle version:
e6a695d
stem + Thread.fork is
further complicated due to requirements for:
* uniform use of bash on all platforms (including Debian/Ubuntu and
Windows)
* proper handling of signals (interrupts)
* management of the external process as a group
* timing informatio
and I would recommend the sequence that Chun Tian posted from Isabelle.
> This is based on my experience with various combinations of the
> distributions together with the experience of Makarius.
It is great when people find re-use of the Isabelle packaging.
Recently I have formalized the P
On 01/03/17 13:55, David Matthews wrote:
>> On 24/02/17 13:26, Makarius wrote:
>> My current guess is that it is a problem of compiled ML code that is no
>> longer garbage-collected.
>
> The current version does garbage collect code; it's just that it only
> happens
On 24/02/17 13:26, Makarius wrote:
> We have strange memory management problems with Isabelle.
>
> I've been using repository versions of Poly/ML privately during the past
> few months, without seeing such problems. Only the official switch in
> http://isabelle.in.tum.de/rep
belle.in.tum.de/repos/isabelle/rev/18f3d341f8c0).
I will come back on that when I've investigated the situation further.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
sets of Poly/ML and consequently of Isabelle/ML.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 20/09/16 14:15, David Matthews wrote:
> On 19/09/2016 21:15, Makarius wrote:
>>> The handling of return addresses from functions has been simplified. A
>>> consequence of this is that when pieces of code are compiled they are
>>> stored in a separate area of mem
On 22/09/16 16:50, David Matthews wrote:
> On 19/09/2016 21:15, Makarius wrote:
>> I am presently testing Poly/ML 38879127481c and Isabelle 9aed2da07200
>> and ran into a compiler problem in src/Pure/unify.ML:
>>
>> Exception- Fail "Exception- InternalError: cho
ed by the character. */
/* This is not infallible but it seems to be good enough
to detect the strings. */
POLYUNSIGNED bytes = length * sizeof(PolyWord);
if (length >= 2 && ...)
It looks like it requires further update.
Makarius
./polyimport --intIsIntInf
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
be some Isabelle/ML programming mishaps in the
application with persistent values that refer to Context.theory instead of
Context.theory_id. Standard containers like the Simplifier or Classical
context take care of that, but add-ons might not.
Makarius
/rev/ad3eb2889f9a
It works fine. I am rather glad that only some ML pretty printing required
a different (approximative) int type.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
ckoverflow further. (It has presently
2 followers and 18 questions.)
It is also possible to vote for questions and answers that are relevant
for Poly/ML, and thus improve its visibility.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
in a few weeks on isabelle-dev
mailing list -- it will have far-reaching consequences to have just one ML
platform.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
hecking, 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
__
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
in 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
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
/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
http
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"
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
Makarius
is always x86-windows.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On Thu, 11 Dec 2014, Peter Gammie wrote:
On 11 Dec 2014, at 4:14, Makarius makar...@sketis.net 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
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 it as
Isabelle session).
Makarius
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 997,299 people so
.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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
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
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
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
/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/listinfo
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
/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 list
polyml
of
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
farm.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
--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
export DYLD_LIBRARY_PATH=$THIS:$DYLD_LIBRARY_PATH
exec $THIS/poly
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
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.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.
Makarius
. social network here.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
. Better use Linux here.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
/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
ago.
Makarius
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
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
signature matching in recent
years.
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
, 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
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 mailing list
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 mailing list
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 substituted
handling in this library.)
Makarius
___
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
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 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
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
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.uk/mailman
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
;
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.ac.uk
http://lists.inf.ed.ac.uk
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 processes. David can
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.output (TextIO.stdOut, Time.toString (Time.now
;
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?
Makarius
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 the Isabelle mailing list.)
Makarius
___
polyml
.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; some years ago many people started to use
.sml and .sig (e.g. in SML/NJ and Moscow ML).
Makarius
? (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
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 ever
had to compile themselves.
Makarius
100 matches
Mail list logo
