Admin/polyml/NOTES
author blanchet
Tue Nov 07 15:16:41 2017 +0100 (20 months ago)
changeset 67021 41f1f8c4259b
parent 66998 8905114fd23b
child 67583 c933a5d4e1ee
permissions -rw-r--r--
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
wenzelm@51061
     1
Notes on building Poly/ML as Isabelle component
wenzelm@51061
     2
===============================================
wenzelm@51061
     3
wenzelm@65880
     4
* component skeleton:
wenzelm@66846
     5
  $ isabelle build_polyml_component -s sha1 component
wenzelm@51061
     6
wenzelm@65880
     7
* include full source (without symlink), for example:
wenzelm@65880
     8
  $ wget https://github.com/polyml/polyml/archive/master.zip
wenzelm@66998
     9
wenzelm@66998
    10
* libgmp on x86_64-darwin:
wenzelm@66998
    11
wenzelm@66998
    12
  https://github.com/Homebrew/homebrew-core/blob/master/Formula/gmp.rb
wenzelm@66998
    13
  https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz
wenzelm@66998
    14
wenzelm@66998
    15
  ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
wenzelm@66998
    16
  make check
wenzelm@66998
    17
  make install
wenzelm@66998
    18
wenzelm@66998
    19
  isabelle build_polyml -m64 -s sha1 src --with-gmp LDFLAGS='-L/usr/local/lib' CPPFLAGS='-O3 -I/usr/local/include'