Poly/ML

polyml@lists.polyml.org

695 discussions

Isabelle/ML IDE (update)
by makarius＠sketis.net 03 Oct '14

03 Oct '14

On Thu, 2 Oct 2014, Tjark Weber wrote: > 1. I suspect that the ITP aspect of Isabelle may put off people who > just want to write SML code. (For instance, there are many documents > and panels visible in the UI that are entirely irrelevant to SML > programming.) If you had unlimited time, I would suggest that the SML > IDE be released separately from Isabelle. This is only the first release of the SML PIDE, but I have started thinking about these questions before. It is probably mainly a matter to re-package the system such that it looks more like an SML IDE outright. Many things are possible, but it also requires some work. Does anybody has smart ideas to find some funding for such projects? It might be also interesting for David Matthews himself, to provide even more IDE support at the bottom, e.g. inclusion of the debugger. We also need to find out how many people are still there to use SML. So far there are already 9 supporters on http://stackoverflow.com/questions/2036744/ml-ide-and-compiler-for-windows-… and the green tick has changed as well :-) > 2. The need to have a theory file (no matter how simple) is slightly > unfortunate. Would an Isabelle/jEdit option "-sml" (or similar) be > feasible to make the enclosing theory redundant, at least for > single-file SML projects? "Unfortunate" (like "fix") is a word of this odd street language that has emerged in recent years and is better ignored. The enclosing theory file is like a project file, but with slightly odd syntax for that purpose, although not too bad compared to the traditional "use" script. There might be other ways emerging to assemble ML files; or maybe just some IDE support to generate such templates. There was also a private discussion with Larry Paulson, to re-use the model of the SML/NJ compilation management, whatever that might be exactly -- we still need to find out. > 3. I noticed that "use" is not available, and that "print" doesn't > affect the output panel. A document that summarizes such differences > (and explains, e.g., how to perform I/O instead) might be useful. Note that "use" is not part of Standard ML. This touches again the question how SML projects are actually managed. For the IDE to work, the control over the ML files needs to be given to the IDE, not the ML program. Further note that "print" is also not Standard ML, although TextIO.print is covered by the Basis Library. That raw stateful output is in conflict with the stateless model of PIDE, but it works as specified: via stdout, which is shown in PIDE in the Raw Output panel. In contrast, the Documentation panel includes src/Tools/SML/Examples.thy with some examples to re-use stateless Isabelle output in SML. > 4. Ctrl+click on certain built-in operators, such as *, takes me to an > empty buffer called "Standard Basis". Surely some explanatory message > could be displayed in the buffer. This information is produced by Poly/ML at the very bottom. E.g. the "length" function refers to $ML_SOURCE/basis/List.sml as expected. David Matthews might be able to tell what happens with * (or +). I know myself from Isabelle/Pure bootstrapping, that formal references to very basic things are sometimes surprising, by construction of the initial environment. Makarius

3 4

Isabelle/ML IDE
by makarius＠sketis.net 29 Sep '14

29 Sep '14

Dear friends of Poly/ML, or Standard ML in general, Isabelle2013-2 is now available from the usual mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ It is mainly an environment for interactive and automated theorem proving, but the integration of Isabelle/ML into the Prover IDE makes it suitable for general Standard ML development (potentially in teaching scenarios). After downloading / unpacking / running the main application 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

1 1

regarding problem with PolyML debugging prompt
by sarojanarayana＠gmail.com 27 Sep '14

27 Sep '14

Hi, I am using PolyML in windows XP sp3 . I tried to run through example on how to use source level debugger, which is provided on you website .http://www.polyml.org/docs/Debugging.html I am able to open debugging prompt using open PolyML.Debug option. But I am unable to exit debug prompt. I tried control C option . But it is only interrupting compilation, without breakIn option as shown in your website. I set breakIn "f" option as mentioned. Please let me the solution. Thanks and regards Saroj

2 1

Motif in Poly/ML: sometimes works, sometimes not
by piotr.trojanek＠gmail.com 01 Sep '14

01 Sep '14

Dear Poly/ML experts, I copy-pasted Motif code from "Poly/ML for Motif: Quick Reference Manual", sections 1.3 and 1.4. When I start poly session and load this code with "use" I sometimes get a Motif window but sometimes do not. I am running polyml 5.5.2 on x86_64 Ubuntu, compiled with "--with-x --enable-shared" against Open Motif 2.3.4. Am I missing something? -- Regards, Piotr Trojanek

2 3

Poly/ML Process Monitor
by tjark.weber＠it.uu.se 20 Aug '14

20 Aug '14

We would like to announce a first version of a graphical process monitoring application for Poly/ML. The monitor displays data regarding, e.g., CPU time, memory footprint, garbage collection and threads of running Poly/ML processes. It is available from https://bitbucket.org/tjark/poly-ml-monitor The monitor is currently available for Linux only. It was written by Magnus Stenqvist and me and relies on Poly/ML's statistics feature, which was implemented by David Matthews. Feedback is welcome. Best, Tjark

1 0

measuring memory usage
by u5028081＠anu.edu.au 18 Aug '14

18 Aug '14

Hi all, Is it possible to measure the memory usage involved in a particular function call from within PolyML 5.5.0? I'm trying to figure out how much memory my vote-counting function uses to count a variety of lists of votes. I'm randomly generating the vote lists, and the functions I'm using for generating the lists seem to use more memory than the count itself. I can't measure what I need with OS tools because they return the memory used to generate the vote lists (because it's larger). I'm not sure where to look for functions of this nature, or if they're even provided in PolyML. Any help appreciated. Thanks in advance, Tom

2 1

can't quit sessions
by u5028081＠anu.edu.au 31 Jul '14

31 Jul '14

Hi all, I'm using PolyML 5.5.0 to run some tests as a batch job and I can't figure out how to quit without using ^D (which I can't feed in automatically when batching things). I've tried using "PolyML.quit ();" and "PolyML.exit 0;" but neither of these work. I'm opening the PolyML structure first (open PolyML;) but I'm still getting errors saying that the commands haven't been declared. I can use some other functions defined in PolyML such as "PolyML.use", but not all (for instance "cd" isn't available). Seems the documentation is incorrect? http://www.polyml.org/docs/Intro1.html Can anyone help me out on this one? Thanks in advance, Tom

2 2

.polyml and poly-stats
by makarius＠sketis.net 02 Jul '14

02 Jul '14

Just a quick question, before I study the Poly/ML sources in detail. What are the conditions under which Poly/ML 5.5.2 creates a directory $HOME/.polyml and puts poly-stats files there? I have recently found by accident that I have hundreds of such files lying around. Maybe I just got some 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

5 8

Poly/ML Array.array segmentation fault
by ramana＠member.fsf.org 09 Jun '14

09 Jun '14

This looks like a bug: % poly Poly/ML 5.5.2 Release > Array.array(~12,4); zsh: segmentation fault (core dumped) poly

2 1

Poly/ML 5.5.2 make fails with linker error
by ykt23＠cam.ac.uk 09 Jun '14

09 Jun '14

I've been trying to build polyML 5.5.2 from the SVN trunk and getting a link error: ./configure --enable-shared ... configure: creating ./config.status config.status: creating include/Makefile config.status: creating include/ffi.h config.status: creating Makefile config.status: creating testsuite/Makefile config.status: creating man/Makefile config.status: creating libffi.pc config.status: creating fficonfig.h config.status: linking src/x86/ffitarget.h to include/ffitarget.h config.status: executing buildir commands config.status: skipping top_srcdir/Makefile - not created config.status: executing depfiles commands config.status: executing libtool commands config.status: executing include commands config.status: executing src commands make make all-recursive make[1]: Entering directory `/home/yongkiam/polymltrunk/polyml' ... mv -f .deps/elfexport.Tpo .deps/elfexport.Plo /bin/bash ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -Wall -O3 -I../libffi/include -MT unix_specific.lo -MD -MP -MF .deps/unix_specific.Tpo -c -o unix_specific.lo unix_specific.cpp libtool: compile: g++ -DHAVE_CONFIG_H -I. -I.. -Wall -O3 -I../libffi/include -MT unix_specific.lo -MD -MP -MF .deps/unix_specific.Tpo -c unix_specific.cpp -fPIC -DPIC -o .libs/unix_specific.o libtool: compile: g++ -DHAVE_CONFIG_H -I. -I.. -Wall -O3 -I../libffi/include -MT unix_specific.lo -MD -MP -MF .deps/unix_specific.Tpo -c unix_specific.cpp -o unix_specific.o >/dev/null 2>&1 mv -f .deps/unix_specific.Tpo .deps/unix_specific.Plo /bin/bash ../libtool --tag=CXX --mode=link g++ -O3 -I../libffi/include -version-info 6:0:0 -o libpolyml.la -rpath /usr/local/lib arb.lo basicio.lo bitmap.lo check_objects.lo diagnostics.lo errors.lo exporter.lo foreign.lo gc.lo gc_check_weak_ref.lo gc_copy_phase.lo gc_mark_phase.lo gc_share_phase.lo gc_update_phase.lo gctaskfarm.lo heapsizing.lo locking.lo memmgr.lo mpoly.lo network.lo objsize.lo osmem.lo pexport.lo poly_specific.lo polystring.lo process_env.lo processes.lo profiling.lo quick_gc.lo realconv.lo reals.lo rts_module.lo run_time.lo save_vec.lo savestate.lo scanaddrs.lo sharedata.lo sighandler.lo statistics.lo timing.lo xwindows.lo x86_dep.lo x86asmtemp.lo elfexport.lo unix_specific.lo ../libffi/libffi_convenience.la -lpthread -lm -ldl -lstdc++ -lgcc_s -lgcc libtool: link: g++ -fPIC -DPIC -shared -nostdlib /usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/crti.o /usr/lib/gcc/x86_64-linux-gnu/4.8/crtbeginS.o .libs/arb.o .libs/basicio.o .libs/bitmap.o .libs/check_objects.o .libs/diagnostics.o .libs/errors.o .libs/exporter.o .libs/foreign.o .libs/gc.o .libs/gc_check_weak_ref.o .libs/gc_copy_phase.o .libs/gc_mark_phase.o .libs/gc_share_phase.o .libs/gc_update_phase.o .libs/gctaskfarm.o .libs/heapsizing.o .libs/locking.o .libs/memmgr.o .libs/mpoly.o .libs/network.o .libs/objsize.o .libs/osmem.o .libs/pexport.o .libs/poly_specific.o .libs/polystring.o .libs/process_env.o .libs/processes.o .libs/profiling.o .libs/quick_gc.o .libs/realconv.o .libs/reals.o .libs/rts_module.o .libs/run_time.o .libs/save_vec.o .libs/savestate.o .libs/scanaddrs.o .libs/sharedata.o .libs/sighandler.o .libs/statistics.o .libs/timing.o .libs/xwindows.o .libs/x86_dep.o .libs/x86asmtemp.o .libs/elfexport.o .libs/unix_specific.o -Wl,--whole-archive ../libffi/.libs/libffi_convenience.a -Wl,--no-whole-archive -lpthread -ldl -lgcc -L/usr/lib/gcc/x86_64-linux-gnu/4.8 -L/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu -L/usr/lib/gcc/x86_64-linux-gnu/4.8/../../../../lib -L/lib/x86_64-linux-gnu -L/lib/../lib -L/usr/lib/x86_64-linux-gnu -L/usr/lib/../lib -L/usr/lib/gcc/x86_64-linux-gnu/4.8/../../.. -lstdc++ -lm -lc -lgcc_s /usr/lib/gcc/x86_64-linux-gnu/4.8/crtendS.o /usr/lib/gcc/x86_64-linux-gnu/4.8/../../../x86_64-linux-gnu/crtn.o -O3 -Wl,-soname -Wl,libpolyml.so.6 -o .libs/libpolyml.so.6.0.0 /usr/bin/ld: .libs/x86asmtemp.o: relocation R_X86_64_PC32 against symbol `X86AsmSaveStateAndReturn' can not be used when making a shared object; recompile with -fPIC /usr/bin/ld: final link failed: Bad value collect2: error: ld returned 1 exit status make[2]: *** [libpolyml.la] Error 1 make[2]: Leaving directory `/home/yongkiam/polymltrunk/polyml/libpolyml' make[1]: *** [all-recursive] Error 1 make[1]: Leaving directory `/home/yongkiam/polymltrunk/polyml' make: *** [all] Error 2

2 1

← Newer
1
...
24
25
26
27
28
29
30
...
70
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML