On 3 Jan 2016, at 18:33, James Clarke <jrtc27 at jrtc27.com> wrote:

Hi Rob, install_pp has been deprecated for a while[1], with addPrettyPrinter[2] being its replacement. Is there a reason you can't use that?

Thanks for the reminder. (I?m glad to see the documentation doesn?t actually say ?deprecated?, a word that I deprecate as a substitute for ?not recommended? :-).) I was actually testing on an oldish release of ProofPower. Later releases use addPrettyPrinter.

Note that the the PolyMLStructure documentation will be out-of-date for version 5.6.

Regards,

Rob.

Regards, James

[1] http://www.polyml.org/documentation/Reference/PolyMLStructure.html#install_p... [2] http://www.polyml.org/documentation/Reference/PolyMLStructure.html#addPretty...

...

On 3 Jan 2016, at 17:27, Rob Arthan <rda at lemma-one.com> wrote:

David,

...

On 2 Jan 2016, at 09:08, David Matthews <David.Matthews at prolingua.co.uk> wrote:

I've updated the github repository with pre-built compilers for 5.6 Release. This is now the release candidate. Unless there are any significant problems this will be released in the next few weeks.

The ProofPower build expects to install pretty-printers using PolyML.install_pp. That doesn?t seem to be there any more in the 5.6 release candidate.

...

Best wishes for 2016,

Happy New Year to you and the Poly/ML user community!

Regards,

Rob. _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

---

polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

I recommend using github markdown in the repository for documentation. Make a top level readme.md file and/or docs directory with documentation. This makes it easy for others to submit pull requests to update improve documentation too.

On Mon, Jan 4, 2016, 16:26 David Matthews <David.Matthews at prolingua.co.uk> wrote:

Rob,

On 04/01/2016 19:44, Rob Arthan wrote:

...

...

On 3 Jan 2016, at 18:33, James Clarke <jrtc27 at jrtc27.com> wrote:

Hi Rob, install_pp has been deprecated for a while[1], with addPrettyPrinter[2] being its replacement. Is there a reason you can't use that?

Thanks for the reminder. (I?m glad to see the documentation doesn?t actually say ?deprecated?, a word that I deprecate as a substitute for ?not recommended? :-).) I was actually testing on an oldish release of ProofPower. Later releases use addPrettyPrinter.

I avoid the use of "deprecated" in that sense although I think it's fair to say it has now acquired a technical meaning and there's no other exact synonym. "Not recommended" doesn't quite capture it.

...

Note that the the PolyMLStructure documentation will be out-of-date for version 5.6.

The Poly/ML documentation was seriously out-of-date or simply non-existent and during the summer I went through and brought it more into line with the version at that stage. It will need some further work.

David _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

On 6 Jan 2016, at 20:41, David Matthews <David.Matthews at prolingua.co.uk> wrote:

Most of the documentation relates to the signatures of library functions. It would be really nice to be able to have the descriptions of the functions contained in comments in the library source itself and then have a program that would automatically turn the ML signature and the special comments into HTML. I think there are such things for other languages although I've never used them. Is there such a thing for ML? This would make it much easier to keep the source code and the documentation in sync.

There once was ml-doc:

http://people.cs.uchicago.edu/~jhr/tools/ml-doc.html

I?ve never used it. IIUC it was used to render the SML basis library manual pages.

haddock (for Haskell) is pretty amazing these days, e.g.

https://hackage.haskell.org/package/base-4.8.1.0/docs/Prelude.html

(I like the ?source? links in particular.)

cheers, peter

On Wed, 6 Jan 2016, David Matthews wrote:

Most of the documentation relates to the signatures of library functions. It would be really nice to be able to have the descriptions of the functions contained in comments in the library source itself and then have a program that would automatically turn the ML signature and the special comments into HTML. I think there are such things for other languages although I've never used them. Is there such a thing for ML? This would make it much easier to keep the source code and the documentation in sync.

Many people think that Isabelle is a theorem prover, but it is actually a document preparation system with formal checking of embedded languages. Isabelle/ML (or Standard ML) is part of that.

That is *not* for pretty printing of raw sources, but for writing regular documents that refer to things defined elsewhere. Output is mainly PDF-LaTeX -- HTML is lagging behind in recent years.

Here is an example:

http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-RC0/src/Doc/I... http://isabelle.in.tum.de/website-Isabelle2016-RC0/dist/Isabelle2016-RC0/doc...

There is also Markdown-like notation: see <^item>, <^enum>, <^descr> in the source, which is rendered with nice Unicode glyphs in the prover IDE. So a realistic view on the source above requires the full application, see http://isabelle.in.tum.de/website-Isabelle2016-RC0

For me, the 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

On 06/01/2016 15:44, Anthony Fox wrote:

When trying to build Poly/ML with

./configure --enabled-shared

I got

ld: illegal text-relocation to 'assign_word' in .libs/x86asmtemp.o from '_entryPointVector' in .libs/x86asmtemp.o for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make[2]: *** [libpolyml.la] Error 1 make[1]: *** [all-recursive] Error 1 make: *** [all] Error 2

However, the build was successful with the default ./configure.

I don't know what is going on here. It looks as though Mac OS X is expecting some sort of relocation rather than an absolute address.

Once built there was a problem when calling polyc, as I was getting the error

ld: unknown option: -R/path/lib

Replacing

-Wl,-R${LIBDIR}

with

-Wl,-rpath ${LIBDIR}

seemed to work (things also worked when I deleted this option). I was then able to build HOL4.

This was added as part of a patch from Aleksej Saushev. The -R option is a synonym for -rpath on Linux/X86. It's not clear whether changing to -rpath would work on all platforms or not. I think the idea was that if Poly/ML was built with a shared library and it was installed to a directory that wasn't in the dynamic library search path having this option would cause polyc to add the installation path into the executable. It's rather nice to have it but if it breaks on some platforms it would be better to remove it.

The warning message

ld: warning: could not create compact unwind for _ffi_call_unix64: does not use RBP or RSP based frame

seems to be back, i.e. it doesn?t go away with -Wl,-no_pie. I?m not sure of the best way to silence this message. I?ve ended up adding -w to EXTRALDFLAGS.

Looking through the log I found that I'd added -Wl,-no_compact_unwind to fix this but then reverted that because it broke exception handling in OS X 10.9.

David

x86asmtemp.S seems to have been compiled as follows:

libtool: compile: gcc -DHAVE_CONFIG_H -I. -I.. -O3 -I../libffi/include -DMACOSX -DGIT_VERSION=8592e2a -Wall -DMODULEDIR=/usr/local/lib/polyml/modules -DMACOSX -MT x86asmtemp.lo -MD -MP -MF .deps/x86asmtemp.Tpo -c x86asmtemp.S -fno-common -DPIC -o .libs/x86asmtemp.o libtool: compile: gcc -DHAVE_CONFIG_H -I. -I.. -O3 -I../libffi/include -DMACOSX -DGIT_VERSION=8592e2a -Wall -DMODULEDIR=/usr/local/lib/polyml/modules -DMACOSX -MT x86asmtemp.lo -MD -MP -MF .deps/x86asmtemp.Tpo -c x86asmtemp.S -o x86asmtemp.o >/dev/null 2>&1

Anthony

On 6 Jan 2016, at 20:24, Jerry James <loganjerry at gmail.com> wrote:

On Wed, Jan 6, 2016 at 11:28 AM, David Matthews <David.Matthews at prolingua.co.uk> wrote:

...

I don't know what is going on here. It looks as though Mac OS X is expecting some sort of relocation rather than an absolute address.

The error means that assign_word is not a position-independent symbol, so the reference to it from _entryPointVector requires a relocation. Anthony, when x86asmtemp.S was compiled, was -fPIC or a related flag passed to the compiler or assembler? (Full disclosure: I don't use, and don't even have access to, Mac OS X, so if I appear to be talking nonsense, that's probably because I am.) -- Jerry James http://www.jamezone.org/

On 06/01/2016 15:44, Anthony Fox wrote:

I?ve been looking into getting HOL4 working with Poly/ML 5.6 (Git version 8592e2a) on Mac OS 10.11.2 with Xcode 7.2.

When trying to build Poly/ML with

./configure --enabled-shared

I got

ld: illegal text-relocation to 'assign_word' in .libs/x86asmtemp.o from '_entryPointVector' in .libs/x86asmtemp.o for architecture x86_64 clang: error: linker command failed with exit code 1 (use -v to see invocation) make[2]: *** [libpolyml.la] Error 1 make[1]: *** [all-recursive] Error 1 make: *** [all] Error 2

I've moved the entryPointVector into the C++ code so it can now be built with position-independent code. It meant adding a lot of external references but it does mean that --enable-shared works on Mac OS X, at least the machine I tried it on.

However, the build was successful with the default ./configure.

Once built there was a problem when calling polyc, as I was getting the error

ld: unknown option: -R/path/lib

Replacing

-Wl,-R${LIBDIR}

with

-Wl,-rpath ${LIBDIR}

I've changed this to use -rpath. It seems to work on the Linux and Mac OS X machines I've tried. I'll take out completely if there are any problems with that.

David

Rob,

On 07/01/2016 17:50, Rob Arthan wrote:

I was wrong about this. Later releases of ProofPower make some use of addPrettyPrinter but still use install_pp. I must have reverted to an earlier version of Poly/ML by mistake and thought things were working under Poly/ML 5.6, when they do not. Not having install_pp will be a stopper for me unless I can roll my own implementation of it using PolyML.addPrettyPrinter. Is that going to be an easy exercise?

The compatibility code for install_pp was removed with a commit on 19th October. See https://github.com/polyml/polyml/commit/075bda98965195f522cf1de02aaf9a6f23d0...

It should give you an idea of what to do but it's very simple because there's a close approximation between the old addString/beginBlock/break/endBlock and PrettyString, PrettyBlock and PrettyBreak. Essentially what it does is create a stack of pending beginBlocks and then adds the breaks and strings to the top of the stack, popping the stack when it finds an endBlock.

You'll have to convert each occurrence of install_pp individually because addPrettyPrinter and the old install_pp are type-dependent functions rather than polymorphic (like PolyML.print).

David