Admin/polyml/NOTES
author wenzelm
Wed, 07 Mar 2018 17:27:57 +0100
changeset 67778 a25f9076a0b3
parent 67583 c933a5d4e1ee
child 72061 0f2ff88f823e
permissions -rw-r--r--
eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;

Notes on building Poly/ML as Isabelle component
===============================================

* component skeleton:
  $ isabelle build_polyml_component -s sha1 component

* include full source (without symlink), for example:
  $ wget https://github.com/polyml/polyml/archive/master.zip