Admin/polyml/NOTES
author haftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70335 9bd8c16b6627
parent 67583 c933a5d4e1ee
child 72061 0f2ff88f823e
permissions -rw-r--r--
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51061
1f184f8ec10b notes on building Poly/ML;
wenzelm
parents:
diff changeset
     1
Notes on building Poly/ML as Isabelle component
1f184f8ec10b notes on building Poly/ML;
wenzelm
parents:
diff changeset
     2
===============================================
1f184f8ec10b notes on building Poly/ML;
wenzelm
parents:
diff changeset
     3
65880
54c6ec4166a4 clarified build_polyml_component;
wenzelm
parents: 65032
diff changeset
     4
* component skeleton:
66846
c04f46a6f29d back to build_polyml_component according to 54c6ec4166a4 (amending 808e6ddb5a50);
wenzelm
parents: 66761
diff changeset
     5
  $ isabelle build_polyml_component -s sha1 component
51061
1f184f8ec10b notes on building Poly/ML;
wenzelm
parents:
diff changeset
     6
65880
54c6ec4166a4 clarified build_polyml_component;
wenzelm
parents: 65032
diff changeset
     7
* include full source (without symlink), for example:
54c6ec4166a4 clarified build_polyml_component;
wenzelm
parents: 65032
diff changeset
     8
  $ wget https://github.com/polyml/polyml/archive/master.zip