diff --git a/Admin/Release/CHECKLIST b/Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST +++ b/Admin/Release/CHECKLIST @@ -1,110 +1,110 @@ Checklist for official releases =============================== - check latest updates of polyml, jdk, scala, jedit; - check Admin/components; - test "isabelle dump -l Pure ZF"; - test "isabelle -o export_theory -f ZF"; - test "isabelle server" according to "system" manual; - test Isabelle/VSCode; - test Isabelle/jEdit: print buffer - test "#!/usr/bin/env isabelle_scala_script"; - test Windows 10 subsystem for Linux: https://docs.microsoft.com/en-us/windows/wsl/install-win10 - check (non-)executable files: $ find . "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" -o -name ROOT ")" -executable $ find -type f -executable - check sources: isabelle check_sources '~~' '$AFP_BASE' isabelle imports -M -a -d '~~/src/Benchmarks' - check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS; - check versions: src/Tools/jEdit/src/Isabelle.props src/Tools/jEdit/src-base/Isabelle_Base.props - check Isabelle version: src/Tools/VSCode/extension/README.md src/Tools/VSCode/extension/package.json - check funny base directory, e.g. "Test 中国"; - check scalable fonts, e.g. src/Doc/Prog_Prove (NOTE: T1 encoding requires cm-super fonts); - diff NEWS wrt. last official release, which is read-only; - update https://bitbucket.org/isabelle_project/isabelle-website - check doc/Contents, src/Tools/jEdit/dist/doc/Contents; - check Logics: ROOTS lib/html/library_index_content.template - HTML library: check HTML header; - HTML library: check theory dependencies (PDF); - check "Handler catches all exceptions" - Mac OS X: check app bundle with Retina display; - Mac OS X: check recent MacTeX; - Windows: check dpi scaling with high-definition display; - Windows: check recent MiKTeX; Repository fork =============== - isabelle: finalize NEWS / CONTRIBUTORS -- proper headers for named release; - isabelle-release: hg tag; - isabelle: back to post-release mode -- after fork point; Packaging ========= - Mac OS X: provide "gnutar" executable via shell PATH (e.g. copy of /usr/bin/gnutar from Mountain Lion) - fully-automated packaging (e.g. on lxbroy10): - hg up -r DISTNAME && Admin/build_release -M macbroy30 -O -l -R DISTNAME /home/isabelle/dist + hg up -r DISTNAME && Admin/build_release -O -l -R DISTNAME /home/isabelle/dist - Docker image: isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2018 Isabelle2018_app.tar.gz https://hub.docker.com/r/makarius/isabelle https://docs.docker.com/docker-cloud/builds/push-images Final release stage =================== - various .hg/hgrc files: default = http://bitbucket.org/isabelle_project/isabelle-release default = ssh://hg@bitbucket.org/isabelle_project/isabelle-release Post-release ============ - update /home/isabelle and /home/isabelle/html-data diff --git a/Admin/components/README b/Admin/components/README --- a/Admin/components/README +++ b/Admin/components/README @@ -1,62 +1,78 @@ -Some notes on maintaining the Isabelle component repository at TUM -================================================================== +Notes on maintaining the Isabelle component repository at TUM +============================================================= Quick reference --------------- - $ install /home/isabelle/components/screwdriver-3.14.tar.gz - $ install /home/isabelle/contrib/screwdriver-3.14/ - $ edit Admin/components/main: screwdriver-3.14 - $ isabelle components_checksum -u - $ hg diff - $ hg commit + * ensure that Isabelle/Scala/SSH can connect to the host specified via + system option "isabelle_components_server"; this may require to install + an unencrypted ssh host key as follows: + + $ ssh-keyscan -t rsa lxbroy10.informatik.tu-muenchen.de >> ~/.ssh/known_hosts + + * local setup (and test) of component directory, e.g. in + + screwdriver-3.14/ + + * packaging (with associated SHA1 digest), e.g. + + $ isabelle build_components screwdriver-3.14 + + * publishing, e.g. + + $ isabelle build_components -P screwdriver-3.14.tar.gz + + * manual editing of Admin/components/main: screwdriver-3.14 Unique names ------------ Component names are globally unique over time and space: names of published components are never re-used. If some component needs to be re-packaged, extra indices may be added to the official version number like this: screwdriver-3.14 #default packaging/publishing, no index screwdriver-3.14-1 #another refinement of the same screwdriver-3.14-2 #yet another refinement of the same There is no standard format for the structure of component names: they are compared for equality only, without any guess at an ordering. Components are registered in Admin/components/main (or similar) for use of that particular Isabelle repository version, subject to regular Mercurial history. This allows to bisect Isabelle versions with full record of the required components for testing. Authentic archives ------------------ Isabelle components are managed as authentic .tar.gz archives in /home/isabelle/components from where they are made publicly available on https://isabelle.in.tum.de/components/. Visibility on the HTTP server depends on local Unix file permission: nonfree components should omit "read" mode for the Unix group/other; regular components should be world-readable. The file Admin/components/components.sha1 contains SHA1 identifiers within the Isabelle repository, for integrity checking of the archives -that are exposed to the public file-system. The components_checksum -tool helps to update these hash-keys wrt. the information within the -Isabelle repository. +that are exposed to the public file-system. The command-line tool +"isabelle build_components" maintains these hash-keys automatically. Unpacked copy ------------- -A second unpacked copy is provided in /home/isabelle/contrib/. This -allows users within the TUM network to activate arbitrary snapshots of -the repository with all standard components being available, without -extra copying or unpacking of the authentic archives. Testing -services like "isatest" and "mira" do this routinely, and will break -accordingly if this is omitted. +A second unpacked copy is provided in /home/isabelle/contrib/. This allows +users and administrative services within the TUM network to activate arbitrary +snapshots of the repository with all standard components being available, +without extra copying or unpacking of the authentic archives. The +isabelle_cronjob does this routinely: it will break if the unpacked version is +omitted. + +The command-line tool "isabelle build_components -P" takes care of uploading +the .tar.gz archive and unpacking it, unless it is a special component (e.g. +for multiplatform application bundling). diff --git a/Admin/components/bundled-macos b/Admin/components/bundled-macos --- a/Admin/components/bundled-macos +++ b/Admin/components/bundled-macos @@ -1,2 +1,2 @@ #additional components to be bundled for release -macos_app-20181205 +macos_app-20181208 diff --git a/Admin/components/components.sha1 b/Admin/components/components.sha1 --- a/Admin/components/components.sha1 +++ b/Admin/components/components.sha1 @@ -1,275 +1,276 @@ +59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz +23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz +eccff31931fb128c1dd522cfc85495c9b66e67af Haskabelle-2015.tar.gz +8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz +847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz +8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz +51e1e0f399e934020565b2301358452c0bcc8a5e ProofGeneral-4.2-2.tar.gz +8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz fbe83b522cb37748ac1b3c943ad71704fdde2f82 bash_process-1.1.1.tar.gz bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz 81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz 97b2491382130a841b3bbaebdcf8720c4d4fb227 bash_process-1.2.2.tar.gz 9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz a65ce644b6094d41e9f991ef851cf05eff5dd0a9 bib2xhtml-20171221.tar.gz f92cff635dfba5d4d77f469307369226c868542c cakeml-2.0.tar.gz e7ffe4238b61a3c1ee87aca4421e7a612e09b836 ci-extras-1.tar.gz 70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz d70bfbe63590153c07709dea7084fbc39c669841 cvc4-1.5-1.tar.gz 541eac340464c5d34b70bb163ae277cc8829c40f cvc4-1.5-2.tar.gz 1a44895d2a440091a15cc92d7f77a06a2e432507 cvc4-1.5-3.tar.gz c0d8d5929b00e113752d8bf5d11241cd3bccafce cvc4-1.5-4.tar.gz +3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz 4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz 76ff6103b8560f0e2778bbfbdb05f5fa18f850b7 cvc4-1.5pre-4.tar.gz 03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz -3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz 842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz 3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz 1fde9ddf0fa4f398965113d0c0c4f0e97c78d008 cygwin-20130716.tar.gz a03735a53c2963eb0b453f6a7282d3419f28bf38 cygwin-20130916.tar.gz 7470125fc46e24ee188bdaacc6d560e01b6fa839 cygwin-20140520.tar.gz db4dedae026981c5f001be283180abc1962b79ad cygwin-20140521.tar.gz acbc4bf161ad21e96ecfe506266ccdbd288f8a6f cygwin-20140530.tar.gz 3dc680d9eb85276e8c3e9f6057dad0efe2d5aa41 cygwin-20140626.tar.gz 8e562dfe57a2f894f9461f4addedb88afa108152 cygwin-20140725.tar.gz 238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf cygwin-20140813.tar.gz 629b8fbe35952d1551cd2a7ff08db697f6dff870 cygwin-20141024.tar.gz ce93d0b3b2743c4f4e5bba30c2889b3b7bc22f2c cygwin-20150410.tar.gz fa712dd5ec66ad16add1779d68aa171ff5694064 cygwin-20151210.tar.gz 056b843d5a3b69ecf8a52c06f2ce6e696dd275f9 cygwin-20151221.tar.gz 44f3a530f727e43a9413226c2423c9ca3e4c0cf5 cygwin-20161002.tar.gz dd56dd16d861fc6e1a008bf5e9da6f33ed6eb820 cygwin-20161022.tar.gz d9ad7aae99d54e3b9813151712eb88a441613f04 cygwin-20161024.tar.gz f8eb6a0f722e3cfe3775d1204c5c7063ee1f008e cygwin-20170828.tar.gz c22048912b010a5a0b4f2a3eb4d318d6953761e4 cygwin-20170930.tar.gz 5a3919e665947b820fd7f57787280c7512be3782 cygwin-20180604.tar.gz 0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz 2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz c11b25c919e2ec44fe2b6ac2086337b456344e97 e-1.8.tar.gz a895a96ec7e6fcc275114bb9b4c92b20fac73dba e-2.0-1.tar.gz 2ebd7e3067a2cdae3cb8b073345827013978d74b e-2.0-2.tar.gz 6b962a6b4539b7ca4199977973c61a8c98a492e8 e-2.0.tar.gz 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz 8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz -59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz -23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz -eccff31931fb128c1dd522cfc85495c9b66e67af Haskabelle-2015.tar.gz 683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz 20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz 736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz 9502c1aea938021f154adadff254c5c55da344bd isabelle_fonts-20151106.tar.gz f5c63689a394b974ac0d365debda577c6fa31c07 isabelle_fonts-20151107.tar.gz 812101680b75f7fa9ee8e138ea6314fa4824ea2d isabelle_fonts-20151229.tar.gz 2730e1475c7d655655882e75743e0b451725a274 isabelle_fonts-20151231.tar.gz 1f004a6bf20088a7e8f1b3d4153aa85de6fc1091 isabelle_fonts-20160101.tar.gz 379d51ef3b71452dac34ba905def3daa8b590f2e isabelle_fonts-20160102.tar.gz 878536aab1eaf1a52da560c20bb41ab942971fa3 isabelle_fonts-20160227.tar.gz 8ff0eedf0191d808ecc58c6b3149a4697f29ab21 isabelle_fonts-20160812-1.tar.gz 9283e3b0b4c7239f57b18e076ec8bb21021832cb isabelle_fonts-20160812.tar.gz 620cffeb125e198b91a716da116f754d6cc8174b isabelle_fonts-20160830.tar.gz b70690c85c05d0ca5bc29287abd20142f6ddcfb0 isabelle_fonts-20171222.tar.gz c17c482e411bbaf992498041a3e1dea80336aaa6 isabelle_fonts-20171230.tar.gz 3affbb306baff37c360319b21cbaa2cc96ebb282 isabelle_fonts-20180113.tar.gz bee32019e5d7cf096ef2ea1d836c732e9a7628cc isabelle_fonts-20181124.tar.gz f249bc2c85bd2af9eee509de17187a766b74ab86 isabelle_fonts-20181129.tar.gz 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz 71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz 8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz 38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz 13a265e4b706ece26fdfa6fc9f4a3dd1366016d2 jdk-7u21.tar.gz 5080274f8721a18111a7f614793afe6c88726739 jdk-7u25.tar.gz dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c jdk-7u40.tar.gz +ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz 71b629b2ce83dbb69967c4785530afce1bec3809 jdk-7u60.tar.gz e119f4cbfa2a39a53b9578d165d0dc44b59527b7 jdk-7u65.tar.gz d6d1c42989433839fe64f34eb77298ef6627aed4 jdk-7u67.tar.gz -ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz b66039bc6dc2bdb2992133743005e1e4fc58ae24 jdk-7u72.tar.gz d980055694ddfae430ee001c7ee877d535e97252 jdk-7u76.tar.gz baa6de37bb6f7a104ce5fe6506bca3d2572d601a jdk-7u80.tar.gz 7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz baf275a68d3f799a841932e4e9a95a1a604058ae jdk-8u102.tar.gz +5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz 741de6a4a805a0f9fb917d1845409e99346c2747 jdk-8u112.tar.gz -5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz ae7df8bd0c18eb40237cf54cc28933f4893b9c92 jdk-8u121.tar.gz 51531a3a0c16e180ed95cb7d2bd680c2ec0aa553 jdk-8u131.tar.gz e45edcf184f608d6f4a7b966d65a5d3289462693 jdk-8u144.tar.gz 264e806b9300a4fb3b6e15ba0e2c664d4ea698c8 jdk-8u152.tar.gz 84b04d877a2ea3a4e2082297b540e14f76722bc5 jdk-8u162.tar.gz 87303a0de3fd595aa3857c8f7cececa036d6ed18 jdk-8u172.tar.gz 9ae0338a5277d8749b4b4c7e65fc627319d98b27 jdk-8u181.tar.gz cfecb1383faaf027ffbabfcd77a0b6a6521e0969 jdk-8u20.tar.gz 44ffeeae219782d40ce6822b580e608e72fd4c76 jdk-8u31.tar.gz +c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz 4132cf52d5025bf330d53b96a5c6466fef432377 jdk-8u51.tar.gz -c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz 74df343671deba03be7caa49de217d78b693f817 jdk-8u60.tar.gz dfb087bd64c3e5da79430e0ba706b9abc559c090 jdk-8u66.tar.gz 2ac389babd15aa5ddd1a424c1509e1c459e6fbb1 jdk-8u72.tar.gz caa0cf65481b6207f66437576643f41dabae3c83 jdk-8u92.tar.gz 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz 9c221fe71af8a063fcffcce21672a97aea0a8d5b jedit_build-20120313.tar.gz ed72630f307729df08fdedb095f0af8725f81b9c jedit_build-20120327.tar.gz 6425f622625024c1de27f3730d6811f6370a19cd jedit_build-20120414.tar.gz 7b012f725ec1cc102dc259df178d511cc7890bba jedit_build-20120813.tar.gz 8e1d36f5071e3def2cb281f7fefe9f52352cb88f jedit_build-20120903.tar.gz 8fa0c67f59beba369ab836562eed4e56382f672a jedit_build-20121201.tar.gz 06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz 5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz 87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz 65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz 30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz 054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz 4a963665537ea66c69de4d761846541ebdbf69f2 jedit_build-20140511.tar.gz a9d637a30f6a87a3583f265da51e63e3619cff52 jedit_build-20140722.tar.gz f29391c53d85715f8454e1aaa304fbccc352928f jedit_build-20141018.tar.gz d7206d4c9d14d3f4c8115422b7391ffbcc6e80b4 jedit_build-20141026.tar.gz f15d36abc1780875a46b6dbd4568e43b776d5db6 jedit_build-20141104.tar.gz 14ce124c897abfa23713928dc034d6ef0e1c5031 jedit_build-20150228.tar.gz b5f7115384c167559211768eb5fe98138864473b jedit_build-20151023.tar.gz 8ba7b6791be788f316427cdcd805daeaa6935190 jedit_build-20151124.tar.gz c70c5a6c565d435a09a8639f8afd3de360708e1c jedit_build-20160330.tar.gz d4e1496c257659cf15458d718f4663cdd95a404e jedit_build-20161024.tar.gz d806c1c26b571b5b4ef05ea11e8b9cf936518e06 jedit_build-20170319.tar.gz 7bcb202e13358dd750e964b2f747664428b5d8b3 jedit_build-20180417.tar.gz 23c8a05687d05a6937f7d600ac3aa19e3ce59c9c jedit_build-20180504.tar.gz 9c64ee0705e5284b507ca527196081979d689519 jedit_build-20181025.tar.gz cfa65bf8720b9b798ffa0986bafbc8437f44f758 jedit_build-20181026.tar.gz 847492b75b38468268f9ea424d27d53f2d95cef4 jedit_build-20181203.tar.gz 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz 2155e0bdbd29cd3d2905454de2e7203b9661d239 jortho-1.0-2.tar.gz ffe179867cf5ffaabbb6bb096db9bdc0d7110065 jortho-1.0.tar.gz 6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz afb04f4048a87bb888fe7b05b0139cb060c7925b kodkodi-1.5.2-1.tar.gz 5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz 377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz 0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz 400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz +3bc42b8e22f0be5ec5614f1914066164c83498f8 macos_app-20181208.tar.gz 26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz 1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz 7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz b3d776e6744f0cd2773d467bc2cfe1de3d1ca2fd polyml-5.5.0-3.tar.gz 1812e9fa6d163f63edb93e37d1217640a166cf3e polyml-5.5.0.tar.gz 36f5b8224f484721749682a3655c796a55a2718d polyml-5.5.1-1.tar.gz 36f78f27291a9ceb13bf1120b62a45625afd44a6 polyml-5.5.1.tar.gz a588640dbf5da9ae15455b02ef709764a48637dc polyml-5.5.2-1.tar.gz 4b690390946f7bfb777b89eb16d6f08987cca12f polyml-5.5.2-2.tar.gz 5b31ad8556e41dfd6d5e85f407818be399aa3d2a polyml-5.5.2-3.tar.gz 532f6e8814752aeb406c62fabcfd2cc05f8a7ca8 polyml-5.5.2.tar.gz 1c53f699d35c0db6c7cf4ea51f2310adbd1d0dc5 polyml-5.5.3-20150820.tar.gz b4b624fb5f34d1dc814fb4fb469fafd7d7ea018a polyml-5.5.3-20150908.tar.gz b668e1f43a41608a8eb365c5e19db6c54c72748a polyml-5.5.3-20150911.tar.gz 1f5cd9b1390dab13861f90dfc06d4180cc107587 polyml-5.5.3-20150916.tar.gz f78896e588e8ebb4da57bf0c95210b0f0fa9e551 polyml-5.6-1.tar.gz +21fa0592b7dfd23269063f42604438165630c0f0 polyml-5.6-2.tar.gz 03ba81e595fa6d6df069532d67ad3195c37d9046 polyml-5.6-20151123.tar.gz 822f489c18e38ce5ef979ec21dccce4473e09be6 polyml-5.6-20151206.tar.gz bd6a448f0e0d5787747f4f30ca661f9c1868e4a7 polyml-5.6-20151223.tar.gz 5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz -21fa0592b7dfd23269063f42604438165630c0f0 polyml-5.6-2.tar.gz 5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz +80b923fca3533bf291ff9da991f2262a98b68cc4 polyml-5.7-20170217.tar.gz 381a70cecf0fdee47f6842e2bdb5107ed52adab6 polyml-5.7.1-1.tar.gz 39dac33b569ac66f76126b8f4edc6d9227bd8a63 polyml-5.7.1-2.tar.gz 0b896ccc35bd3f2541cd55e6f0ed14637ed9fc68 polyml-5.7.1-4.tar.gz 262450ac9966abebae2e1d4f9ae703cfe0f5d8d9 polyml-5.7.1-5.tar.gz 1aeb57877d694db7fe4d4395287cddf3bc77710b polyml-5.7.1-6.tar.gz e3e7e20b1e0e5d5d68df4cd4caa1e1a7410d46b6 polyml-5.7.1-7.tar.gz 1430533c09b17f8be73798a47a5f409d43a04cf4 polyml-5.7.1-8.tar.gz 171b5783b88522a35e4822b19ef8ba838c04f494 polyml-5.7.1.tar.gz -80b923fca3533bf291ff9da991f2262a98b68cc4 polyml-5.7-20170217.tar.gz 5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz 4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz 853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz 2b7c02b67feb2f44dda6938a7244f4257e7c580c polyml-test-905dae2ebfda.tar.gz b4ceeaac47f3baae41c2491a8368b03217946166 polyml-test-e7a662f8f9c4.tar.gz 609c7d09d3ed01156ff91261e801e2403ff93729 polyml-test-e8d82343b692.tar.gz a619177143fea42a464f49bb864665407c07a16c polyml-test-fb4f42af00fa.tar.gz 53123dc011b2d4b4e8fe307f3c9fa355718ad01a postgresql-42.1.1.tar.gz 3a5d31377ec07a5069957f5477a4848cfc89a594 postgresql-42.1.4.tar.gz e7cd5c7955e9eb5ce8cd07feb97230b23d2eec40 postgresql-42.2.2.tar.gz 231b33c9c3c27d47e3ba01b399103d70509e0731 postgresql-42.2.5.tar.gz f132329ca1045858ef456cc08b197c9eeea6881b postgresql-9.4.1212.tar.gz -8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz -847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz -8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz -51e1e0f399e934020565b2301358452c0bcc8a5e ProofGeneral-4.2-2.tar.gz -8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz 0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc scala-2.10.1.tar.gz 207e4916336335386589c918c5e3f3dcc14698f2 scala-2.10.2.tar.gz 21c8ee274ffa471ab54d4196ecd827bf3d43e591 scala-2.10.3.tar.gz d4688ddaf83037ca43b5bf271325fc53ae70e3aa scala-2.10.4.tar.gz 44d12297a78988ffd34363535e6a8e0d94c1d8b5 scala-2.11.0.tar.gz 14f20de82b25215a5e055631fb147356400625e6 scala-2.11.1.tar.gz 4fe9590d08e55760b86755d3fab750e90ac6c380 scala-2.11.2.tar.gz 27a296495b2167148de06314ed9a942f2dbe23fe scala-2.11.4.tar.gz 4b24326541161ce65424293ca9da3e7c2c6ab452 scala-2.11.5.tar.gz e7cf20e3b27c894c6127c7a37042c1667f57385e scala-2.11.6.tar.gz 4810c1b00719115df235be1c5991aa6ea7186134 scala-2.11.7.tar.gz 3eca4b80710996fff87ed1340dcea2c5f6ebf4f7 scala-2.11.8.tar.gz 0004e53f885fb165b50c95686dec40d99ab0bdbd scala-2.12.0.tar.gz 74a8c3dab3a25a87357996ab3e95d825dc820fd0 scala-2.12.2.tar.gz d66796a68ec3254b46b17b1f8ee5bcc56a93aacf scala-2.12.3.tar.gz 1636556167dff2c191baf502c23f12e09181ef78 scala-2.12.4.tar.gz 8171f494bba54fb0d01c887f889ab8fde7171c2a scala-2.12.5.tar.gz 54c1b06fa2c5f6c2ab3d391ef342c0532cd7f392 scala-2.12.6.tar.gz 02358f00acc138371324b6248fdb62eed791c6bd scala-2.12.7.tar.gz b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz 5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz cbd491c0feba1d21019d05564e76dd04f592ccb4 spass-3.8ds-1.tar.gz 43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz b016a785f1f78855c00d351ff598355c3b87450f sqlite-jdbc-3.18.0-1.tar.gz b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz e56117a67ab01fb24c7fc054ede3160cefdac5f8 sqlite-jdbc-3.20.0.tar.gz 27aeac6a91353d69f0438837798ac4ae6f9ff8c5 sqlite-jdbc-3.23.1.tar.gz 8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz 2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz fdc415284e031ee3eb2f65828cbc6945736fe995 stack-1.9.1.tar.gz 6e19948ff4a821e2052fc9b3ddd9ae343f4fcdbb stack-1.9.3.tar.gz 1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz 601e08d048d8e50b0729429c8928b667d9b6bde9 sumatra_pdf-2.3.2.tar.gz 14d46c2eb1a34821703da59d543433f581e91df3 sumatra_pdf-2.4.tar.gz 44d67b6742919ce59a42368fc60e2afa210a3e42 sumatra_pdf-2.5.2.tar.gz 89719a13bc92810730a430973684629426ed1b2a sumatra_pdf-3.0.tar.gz f5afcc82f8e734665d38867e99475d3ad0d5ed15 sumatra_pdf-3.1.1.tar.gz 8486387f61557147ec06b1f637117c017c8f0528 sumatra_pdf-3.1.2.tar.gz 869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz 399f687b56575b93e730f68c91c989cb48aa34d8 vampire-4.2.2.tar.gz 98c5c79fef7256db9f64c8feea2edef0a789ce46 verit-2016post.tar.gz 81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz 8fe004aead867d4c82425afac481142bd3f01fb0 windows_app-20130908.tar.gz d273abdc7387462f77a127fa43095eed78332b5c windows_app-20130909.tar.gz c368908584e2bca38b3bcb20431d0c69399fc2f0 windows_app-20131130.tar.gz c3f5285481a95fde3c1961595b4dd0311ee7ac1f windows_app-20131201.tar.gz 14807afcf69e50d49663d5b48f4b103f30ae842b windows_app-20150821.tar.gz ed106181510e825bf959025d8e0a2fc3f78e7a3f windows_app-20180417.tar.gz e809e4ab0d33cb413a7c47dd947e7dbdfcca1c24 windows_app-20181002.tar.gz 9e96ba128a0617a9020a178781df49d48c997e19 windows_app-20181006.tar.gz 1c36a840320dfa9bac8af25fc289a4df5ea3eccb xz-java-1.2-1.tar.gz 2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz c22196148fcace5443a933238216cff5112948df xz-java-1.5.tar.gz 4368ee09154dff42666a8c87e072261745619e51 xz-java-1.6.tar.gz 63f5fa09e92a895cb9aea27d7142abc86c487d25 xz-java-1.8.tar.gz 4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz 3a8f77822278fe9250890e357248bc678d8fac95 z3-3.2-1.tar.gz 12ae71acde43bd7bed1e005c43034b208c0cba4c z3-3.2.tar.gz d94a716502c8503d63952bcb4d4176fac8b28704 z3-4.0.tar.gz 86e721296c400ada440e4a9ce11b9e845eec9e25 z3-4.3.0.tar.gz a8917c31b31c182edeec0aaa48870844960c8a61 z3-4.3.2pre-1.tar.gz 06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz 93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8 z3-4.4.0pre-1.tar.gz b1bc411c2083fc01577070b56b94514676f53854 z3-4.4.0pre-2.tar.gz 517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz diff --git a/Admin/etc/options b/Admin/etc/options new file mode 100644 --- /dev/null +++ b/Admin/etc/options @@ -0,0 +1,12 @@ +(* :mode=isabelle-options: *) + +section "Admin tools" + +option isabelle_components_server : string = "lxbroy10.informatik.tu-muenchen.de" + -- "user@host for SSH connection" + +option isabelle_components_dir : string = "/home/isabelle/components" + -- "webspace for ISABELLE_COMPONENT_REPOSITORY" + +option isabelle_components_contrib_dir : string = "/home/isabelle/contrib" + -- "unpacked components for remote build services" diff --git a/Admin/lib/Tools/components_checksum b/Admin/lib/Tools/components_checksum deleted file mode 100755 --- a/Admin/lib/Tools/components_checksum +++ /dev/null @@ -1,80 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Alexander Krauss -# -# DESCRIPTION: compute and validate checksums for component repository - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: $PRG [OPTIONS] [DIR]" - echo - echo " Options are:" - echo " -u update the recorded checksums in the repository" - echo " -c compare the actual checksums with the recorded ones" - echo - echo " Compute the checksums of component .tar.gz archives in DIR" - echo " (default \"/home/isabelle/components\") and synchronize them" - echo " with the Isabelle repository." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -# options - -UPDATE="" -CHECK="" -COMPONENTS_DIR="/home/isabelle/components" - -while getopts "uc" OPT -do - case "$OPT" in - u) - UPDATE=true - ;; - c) - CHECK=true - ;; - esac -done - -shift $(($OPTIND - 1)) - -[ -n "$UPDATE" ] || [ -n "$CHECK" ] || usage - - -# args - -[ "$#" -ge 1 ] && { COMPONENTS_DIR="$1"; shift; } -[ "$#" -ne 0 ] && usage - - -## compute checksums - -CHECKSUM_DIR="$ISABELLE_HOME/Admin/components" -CHECKSUM_FILE="$CHECKSUM_DIR/components.sha1" -CHECKSUM_TMP="$CHECKSUM_DIR/components.sha1.tmp" - -( - cd "$COMPONENTS_DIR" - sha1sum *.tar.gz | sort -k2 -f > "$CHECKSUM_TMP" -) - -[ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE" -[ -n "$CHECK" ] && { - diff "$CHECKSUM_FILE" "$CHECKSUM_TMP" || fail "Integrity error" -} diff --git a/etc/options b/etc/options --- a/etc/options +++ b/etc/options @@ -1,286 +1,286 @@ (* :mode=isabelle-options: *) section "Document Preparation" option browser_info : bool = false -- "generate theory browser information" option document : string = "" -- "build document in given format: pdf, dvi, false" option document_output : string = "" -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" option document_variants : string = "document" -- "alternative document variants (separated by colons)" option document_tags : string = "" -- "default command tags (separated by commas)" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" option thy_output_break : bool = false -- "control line breaks in non-display material" option thy_output_quotes : bool = false -- "indicate if the output should be enclosed in double quotes" option thy_output_margin : int = 76 -- "right margin / page width for printing of display material" option thy_output_indent : int = 0 -- "indentation for pretty printing of display material" option thy_output_source : bool = false -- "print original source text rather than internal representation" option thy_output_modes : string = "" -- "additional print modes for document output (separated by commas)" section "Prover Output" option show_types : bool = false -- "show type constraints when printing terms" option show_sorts : bool = false -- "show sort constraints when printing types" option show_brackets : bool = false -- "show extra brackets when printing terms/types" option show_question_marks : bool = true -- "show leading question mark of schematic variables" option show_consts : bool = false -- "show constants with types when printing proof state" option show_main_goal : bool = false -- "show main goal when printing proof state" option goals_limit : int = 10 -- "maximum number of subgoals to be printed" option names_long : bool = false -- "show fully qualified names" option names_short : bool = false -- "show base names only" option names_unique : bool = true -- "show partially qualified names, as required for unique name resolution" option eta_contract : bool = true -- "print terms in eta-contracted form" option print_mode : string = "" -- "additional print modes for prover output (separated by commas)" section "Parallel Processing" public option threads : int = 0 -- "maximum number of worker threads for prover process (0 = hardware max.)" option threads_trace : int = 0 -- "level of tracing information for multithreading" option threads_stack_limit : real = 0.25 -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" public option parallel_limit : int = 0 -- "approximative limit for parallel tasks (0 = unlimited)" public option parallel_print : bool = true -- "parallel and asynchronous printing of results" public option parallel_proofs : int = 1 -- "level of parallel proof checking: 0, 1, 2" option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" option command_timing_threshold : real = 0.1 -- "default threshold for persistent command timing (seconds)" section "Detail of Proof Checking" option record_proofs : int = -1 -- "set level of proofterm recording: 0, 1, 2, negative means unchanged" option quick_and_dirty : bool = false -- "if true then some tools will OMIT some proofs" option skip_proofs : bool = false -- "skip over proofs (implicit 'sorry')" option strict_facts : bool = false -- "force lazy facts when defined in context" section "Global Session Parameters" option condition : string = "" -- "required environment variables for subsequent theories (separated by commas)" option timeout : real = 0 -- "timeout for session build job (seconds > 0)" option timeout_scale : real = 1.0 -- "scale factor for session timeout" option process_output_limit : int = 100 -- "build process output limit (in million characters, 0 = unlimited)" option process_output_tail : int = 40 -- "build process output tail shown to user (in lines, 0 = unlimited)" option checkpoint : bool = false -- "checkpoint for theories during build process (heap compression)" option profiling : string = "" -- "ML profiling (possible values: time, allocations)" section "ML System" option ML_print_depth : int = 20 -- "ML print depth for toplevel pretty-printing" public option ML_exception_trace : bool = false -- "ML exception trace for toplevel command execution" public option ML_exception_debugger : bool = false -- "ML debugger exception trace for toplevel command execution" public option ML_debugger : bool = false -- "ML debugger instrumentation for newly compiled code" public option ML_statistics : bool = true -- "ML run-time system statistics" public option ML_system_64 : bool = false -- "ML system for 64bit platform is used if possible (change requires restart)" public option ML_process_policy : string = "" -- "ML process command prefix (process policy)" section "Editor Reactivity" public option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)" public option editor_input_delay : real = 0.3 -- "delay for user input (text edits, cursor movement etc.)" public option editor_generated_input_delay : real = 1.0 -- "delay for machine-generated input that may outperform user edits" public option editor_output_delay : real = 0.1 -- "delay for prover output (markup, common messages etc.)" public option editor_consolidate_delay : real = 2.0 -- "delay to consolidate status of command evaluation (execution forks)" public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" option editor_prune_size : int = 0 -- "retained size of pruned history (delete old versions)" public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates" public option editor_reparse_limit : int = 10000 -- "maximum amount of reparsed text outside perspective" public option editor_tracing_messages : int = 1000 -- "initial number of tracing messages for each command transaction (0: unbounded)" public option editor_chart_delay : real = 3.0 -- "delay for chart repainting" public option editor_continuous_checking : bool = true -- "continuous checking of proof document (visible and required parts)" public option editor_output_state : bool = false -- "implicit output of proof state" option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" option editor_syslog_limit : int = 100 -- "maximum amount of buffered syslog messages" public option editor_presentation : bool = false -- "dynamic presentation while editing" section "Miscellaneous Tools" public option find_theorems_limit : int = 40 -- "limit of displayed results" public option find_theorems_tactic_limit : int = 5 -- "limit of tactic search for 'solves' criterion" section "Completion" public option completion_limit : int = 40 -- "limit for completion within the formal context" public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" -- "glob patterns to ignore in file-system path completion (separated by colons)" section "Spell Checker" public option spell_checker : bool = true -- "enable spell-checker for prose words within document text, comments etc." public option spell_checker_dictionary : string = "en" -- "spell-checker dictionary name" public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" -- "included markup elements for spell-checker (separated by commas)" public option spell_checker_exclude : string = "no_words,antiquoted" -- "excluded markup elements for spell-checker (separated by commas)" section "Secure Shell" -option ssh_config_dir : string = "~/.ssh" +option ssh_config_dir : string = "$HOME/.ssh" -- "SSH configuration directory" -option ssh_config_file : string = "~/.ssh/config" +option ssh_config_file : string = "$HOME/.ssh/config" -- "main SSH configuration file" -option ssh_identity_files : string = "~/.ssh/id_dsa:~/.ssh/id_ecdsa:~/.ssh/id_rsa" +option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa" -- "possible SSH identity files (separated by colons)" option ssh_compression : bool = true -- "enable SSH compression" option ssh_connect_timeout : real = 60 -- "SSH connection timeout (seconds)" option ssh_alive_interval : real = 30 -- "time interval to keep SSH server connection alive (seconds)" option ssh_alive_count_max : int = 3 -- "maximum number of messages to keep SSH server connection alive" section "Theory Export" option export_document : bool = false option export_theory : bool = false section "Build Database" option build_database_server : bool = false option build_database_user : string = "" option build_database_password : string = "" option build_database_name : string = "" option build_database_host : string = "" option build_database_port : int = 0 option build_database_ssh_host : string = "" option build_database_ssh_user : string = "" option build_database_ssh_port : int = 0 section "Build Log Database" option build_log_database_user : string = "" option build_log_database_password : string = "" option build_log_database_name : string = "" option build_log_database_host : string = "" option build_log_database_port : int = 0 option build_log_ssh_host : string = "" option build_log_ssh_user : string = "" option build_log_ssh_port : int = 0 option build_log_history : int = 30 -- "length of relevant history (in days)" option build_log_transaction_size : int = 1 -- "number of log files for each db update" diff --git a/src/Pure/Admin/build_cygwin.scala b/src/Pure/Admin/build_cygwin.scala --- a/src/Pure/Admin/build_cygwin.scala +++ b/src/Pure/Admin/build_cygwin.scala @@ -1,90 +1,89 @@ /* Title: Pure/Admin/build_cygwin.scala Author: Makarius Produce pre-canned Cygwin distribution for Isabelle. */ package isabelle object Build_Cygwin { val default_mirror: String = "https://isabelle.sketis.net/cygwin_2018" val packages: List[String] = List("curl", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip") def build_cygwin(progress: Progress, mirror: String = default_mirror, more_packages: List[String] = Nil) { require(Platform.is_windows) Isabelle_System.with_tmp_dir("cygwin")(tmp_dir => { val cygwin = tmp_dir + Path.explode("cygwin") val cygwin_etc = cygwin + Path.explode("etc") val cygwin_isabelle = cygwin + Path.explode("isabelle") Isabelle_System.mkdirs(cygwin_isabelle) val cygwin_exe_name = mirror + "/setup-x86_64.exe" val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe") Bytes.write(cygwin_exe, try { Bytes.read(Url(cygwin_exe_name)) } catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) }) File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror) File.executable(cygwin_exe) Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h /dev/null").check val res = progress.bash( File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" + " --local-package-dir 'C:\\temp'" + " --root " + Bash.string(File.platform_path(cygwin)) + " --packages " + quote((packages ::: more_packages).mkString(",")) + " --no-shortcuts --no-startmenu --no-desktop --quiet-mode", echo = true) if (!res.ok || !cygwin_etc.is_dir) error("Failed") for (name <- List("hosts", "protocols", "services", "networks", "passwd", "group")) (cygwin_etc + Path.explode(name)).file.delete (cygwin + Path.explode("Cygwin.bat")).file.delete val archive = "cygwin-" + Date.Format("uuuuMMdd")(Date.now()) + ".tar.gz" - Isabelle_System.gnutar("-C " + File.bash_path(tmp_dir) + - " -czf " + Bash.string(archive) + " cygwin").check + Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle", args => { var mirror = default_mirror var more_packages: List[String] = Nil val getopts = Getopts(""" Usage: isabelle build_cygwin [OPTIONS] Options are: -R MIRROR Cygwin mirror site (default """ + quote(default_mirror) + """) -p NAME additional Cygwin package Produce pre-canned Cygwin distribution for Isabelle: this requires Windows administrator mode. """, "R:" -> (arg => mirror = arg), "p:" -> (arg => more_packages ::= arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages) }) } diff --git a/src/Pure/Admin/build_jdk.scala b/src/Pure/Admin/build_jdk.scala --- a/src/Pure/Admin/build_jdk.scala +++ b/src/Pure/Admin/build_jdk.scala @@ -1,240 +1,240 @@ /* Title: Pure/Admin/build_jdk.scala Author: Makarius Build Isabelle jdk component from original platform installations. */ package isabelle import java.io.{File => JFile} import java.nio.file.Files import java.nio.file.attribute.PosixFilePermission import scala.util.matching.Regex object Build_JDK { /* version */ def detect_version(s: String): String = { val Version_Dir_Entry = """^jdk-(\d+\+\d+)$""".r s match { case Version_Dir_Entry(version) => version case _ => error("Cannot detect JDK version from " + quote(s)) } } /* platform */ sealed case class JDK_Platform(name: String, home: String, exe: String, regex: Regex) { override def toString: String = name def detect(jdk_dir: Path): Boolean = { val path = jdk_dir + Path.explode(exe) if (path.is_file) { val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out regex.pattern.matcher(file_descr).matches } else false } } val jdk_platforms = List( JDK_Platform("x86_64-linux", ".", "bin/java", """.*ELF 64-bit.*x86[-_]64.*""".r), JDK_Platform("x86_64-windows", ".", "bin/java.exe", """.*PE32\+ executable.*x86[-_]64.*""".r), JDK_Platform("x86_64-darwin", "Contents/Home", "Contents/Home/bin/java", """.*Mach-O 64-bit.*x86[-_]64.*""".r)) /* README */ def readme(version: String): String = """This is OpenJDK """ + version + """ as required for Isabelle. See https://adoptopenjdk.net for the original downloads, which are covered the GPL2 (with various liberal exceptions, see legal/*). Linux, Windows, Mac OS X all work uniformly, depending on certain platform-specific subdirectories. """ /* settings */ val settings = """# -*- shell-script -*- :mode=shellscript: case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; windows) ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; macos) ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM/Contents/Home" ;; esac """ /* extract archive */ private def suppress_name(name: String): Boolean = name.startsWith("._") def extract_archive(dir: Path, archive: Path): (String, JDK_Platform) = { try { val tmp_dir = dir + Path.explode("tmp") Isabelle_System.mkdirs(tmp_dir) if (archive.get_ext == "zip") { Isabelle_System.bash( "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check } else { - Isabelle_System.gnutar( - "-C " + File.bash_path(tmp_dir) + " -xzf " + File.bash_path(archive)).check + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check } val dir_entry = File.read_dir(tmp_dir).filterNot(suppress_name(_)) match { case List(s) => s case _ => error("Archive contains multiple directories") } val version = detect_version(dir_entry) val jdk_dir = tmp_dir + Path.explode(dir_entry) val platform = jdk_platforms.find(_.detect(jdk_dir)) getOrElse error("Failed to detect JDK platform") val platform_dir = dir + Path.explode(platform.name) if (platform_dir.is_dir) error("Directory already exists: " + platform_dir) File.link(Path.current, jdk_dir + Path.explode(platform.home) + Path.explode("jre")) File.move(jdk_dir, platform_dir) (version, platform) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) } } /* build jdk */ def build_jdk( archives: List[Path], progress: Progress = No_Progress, target_dir: Path = Path.current) { if (Platform.is_windows) error("Cannot build jdk on Windows") Isabelle_System.with_tmp_dir("jdk")(dir => { progress.echo("Extracting ...") val extracted = archives.map(extract_archive(dir, _)) val version = extracted.map(_._1).toSet.toList match { case List(version) => version case Nil => error("No archives") case versions => error("Archives contain multiple JDK versions: " + commas_quote(versions)) } val missing_platforms = jdk_platforms.filterNot(p1 => extracted.exists({ case (_, p2) => p1.name == p2.name })) if (missing_platforms.nonEmpty) error("Missing platforms: " + commas_quote(missing_platforms.map(_.name))) val jdk_name = "jdk-" + version val jdk_path = Path.explode(jdk_name) val component_dir = dir + jdk_path Isabelle_System.mkdirs(component_dir + Path.explode("etc")) File.write(Components.settings(component_dir), settings) File.write(component_dir + Path.explode("README"), readme(version)) for ((_, platform) <- extracted) File.move(dir + Path.explode(platform.name), component_dir) for (file <- File.find_files(component_dir.file, include_dirs = true)) { val path = file.toPath val perms = Files.getPosixFilePermissions(path) perms.add(PosixFilePermission.OWNER_READ) perms.add(PosixFilePermission.GROUP_READ) perms.add(PosixFilePermission.OTHERS_READ) perms.add(PosixFilePermission.OWNER_WRITE) if (file.isDirectory) { perms.add(PosixFilePermission.OWNER_WRITE) perms.add(PosixFilePermission.OWNER_EXECUTE) perms.add(PosixFilePermission.GROUP_EXECUTE) perms.add(PosixFilePermission.OTHERS_EXECUTE) } Files.setPosixFilePermissions(path, perms) } File.find_files((component_dir + Path.explode("x86_64-darwin")).file, file => suppress_name(file.getName)).foreach(_.delete) progress.echo("Sharing ...") val main_dir :: other_dirs = jdk_platforms.map(platform => (component_dir + Path.explode(platform.name)).file.toPath) for { file1 <- File.find_files(main_dir.toFile).iterator path1 = file1.toPath dir2 <- other_dirs.iterator } { val path2 = dir2.resolve(main_dir.relativize(path1)) val file2 = path2.toFile if (!Files.isSymbolicLink(path2) && file2.isFile && File.eq_content(file1, file2)) { file2.delete Files.createLink(path2, path1) } } progress.echo("Archiving ...") - Isabelle_System.gnutar("--owner=root --group=root -C " + File.bash_path(dir) + - " -czf " + File.bash_path(target_dir + jdk_path.ext("tar.gz")) + " " + jdk_name).check + Isabelle_System.gnutar( + "-czf " + File.bash_path(target_dir + jdk_path.ext("tar.gz")) + " " + jdk_name, + dir = dir).check }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives", args => { var target_dir = Path.current val getopts = Getopts(""" Usage: isabelle build_jdk [OPTIONS] ARCHIVES... Options are: -D DIR target directory (default ".") Build jdk component from tar.gz archives, with original jdk archives for x86_64 Linux, Windows, Mac OS X. """, "D:" -> (arg => target_dir = Path.explode(arg))) val more_args = getopts(args) if (more_args.isEmpty) getopts.usage() val archives = more_args.map(Path.explode(_)) val progress = new Console_Progress() build_jdk(archives = archives, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala +++ b/src/Pure/Admin/build_release.scala @@ -1,811 +1,776 @@ /* Title: Pure/Admin/build_release.scala Author: Makarius Build full Isabelle distribution from repository. */ package isabelle object Build_Release { /** release info **/ sealed case class Bundle_Info( platform: Platform.Family.Value, platform_description: String, - main: String, - fallback: Option[String]) + name: String) { - def names: List[String] = main :: fallback.toList + def path: Path = Path.explode(name) } class Release private[Build_Release]( progress: Progress, val date: Date, val dist_name: String, val dist_dir: Path, val dist_version: String, val ident: String) { val isabelle_dir: Path = dist_dir + Path.explode(dist_name) val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") def other_isabelle(dir: Path): Other_Isabelle = Other_Isabelle(dir + Path.explode(dist_name), isabelle_identifier = dist_name + "-build", progress = progress) def bundle_info(platform: Platform.Family.Value): Bundle_Info = platform match { - case Platform.Family.linux => - Bundle_Info(platform, "Linux", dist_name + "_app.tar.gz", None) - case Platform.Family.macos => - Bundle_Info(platform, "Mac OS X", dist_name + ".dmg", Some(dist_name + "_dmg.tar.gz")) - case Platform.Family.windows => - Bundle_Info(platform, "Windows", dist_name + ".exe", None) + case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz") + case Platform.Family.macos => Bundle_Info(platform, "Mac OS X", dist_name + "_macos.tar.gz") + case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe") } } /** generated content **/ /* patch release */ private def change_file(dir: Path, name: String, f: String => String) { val file = dir + Path.explode(name) File.write(file, f(File.read(file))) } private val getsettings_file: String = "lib/scripts/getsettings" private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r def patch_release(release: Release, is_official: Boolean) { val dir = release.isabelle_dir for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala")) { change_file(dir, name, s => s.replaceAllLiterally("val is_identified = false", "val is_identified = true") .replaceAllLiterally("val is_official = false", "val is_official = " + is_official)) } change_file(dir, getsettings_file, s => s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident)) .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name))) change_file(dir, "lib/html/library_index_header.template", s => s.replaceAllLiterally("{ISABELLE}", release.dist_name)) for { name <- List( "src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala", "lib/Tools/version") } { change_file(dir, name, s => s.replaceAllLiterally("repository version", release.dist_version)) } change_file(dir, "README", s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version)) } /* ANNOUNCE */ def make_announce(release: Release) { File.write(release.isabelle_dir + Path.explode("ANNOUNCE"), """ IMPORTANT NOTE ============== This is a snapshot of Isabelle/""" + release.ident + """ from the repository. """) } /* NEWS */ def make_news(other_isabelle: Other_Isabelle, dist_version: String) { val target = other_isabelle.isabelle_home + Path.explode("doc") val target_fonts = target + Path.explode("fonts") Isabelle_System.mkdirs(target_fonts) other_isabelle.copy_fonts(target_fonts) HTML.write_document(target, "NEWS.html", List(HTML.title("NEWS (" + dist_version + ")")), List( HTML.chapter("NEWS"), HTML.source( Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS")))))) } /* bundled components */ class Bundled(platform: Option[Platform.Family.Value] = None) { def detect(s: String): Boolean = s.startsWith("#bundled") && !s.startsWith("#bundled ") def apply(name: String): String = "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name private val Pattern1 = ("""^#bundled:(.*)$""").r private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r def unapply(s: String): Option[String] = s match { case Pattern1(name) => Some(name) case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name) case _ => None } } def record_bundled_components(dir: Path) { val catalogs = List("main", "bundled").map((_, new Bundled())) ::: default_platform_families.flatMap(platform => List(platform.toString, "bundled-" + platform.toString). map((_, new Bundled(platform = Some(platform))))) File.append(Components.components(dir), terminate_lines("#bundled components" :: (for { (catalog, bundled) <- catalogs.iterator val path = Components.admin(dir) + Path.basic(catalog) if path.is_file line <- split_lines(File.read(path)) if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build") } yield bundled(line)).toList)) } def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = { val Bundled = new Bundled(platform = Some(platform)) val components = for { Bundled(name) <- Components.read_components(dir) if !name.startsWith("jedit_build") } yield name val jdk_component = components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") (components, jdk_component) } def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String]) { def contrib_name(name: String): String = Components.contrib(name = name).implode val Bundled = new Bundled(platform = Some(platform)) Components.write_components(dir, Components.read_components(dir).flatMap(line => line match { case Bundled(name) => if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) else None case _ => if (Bundled.detect(line)) None else Some(line) }) ::: more_names.map(contrib_name(_))) } def make_contrib(dir: Path) { Isabelle_System.mkdirs(Components.contrib(dir)) File.write(Components.contrib(dir, "README"), """This directory contains add-on components that contribute to the main Isabelle distribution. Separate licensing conditions apply, see each directory individually. """) } /** build_release **/ private def execute(dir: Path, script: String): Unit = Isabelle_System.bash(script, cwd = dir.file).check private def execute_tar(dir: Path, args: String): Unit = - Isabelle_System.gnutar(args, cwd = dir.file).check - - private def tar_options: String = - if (Platform.is_macos) "--owner=root --group=staff" else "--owner=root --group=root" + Isabelle_System.gnutar(args, dir = dir).check private val default_platform_families: List[Platform.Family.Value] = List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos) def build_release(base_dir: Path, options: Options, components_base: Option[Path] = None, progress: Progress = No_Progress, rev: String = "", afp_rev: String = "", official_release: Boolean = false, proper_release_name: Option[String] = None, platform_families: List[Platform.Family.Value] = default_platform_families, more_components: List[Path] = Nil, website: Option[Path] = None, build_library: Boolean = false, - parallel_jobs: Int = 1, - remote_mac: String = ""): Release = + parallel_jobs: Int = 1): Release = { val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) val release = { val date = Date.now() val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date)) val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute val version = proper_string(rev) orElse proper_release_name getOrElse "tip" val ident = try { hg.id(version) } catch { case ERROR(_) => error("Bad repository version: " + version) } val dist_version = proper_release_name match { case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date) case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date) } new Release(progress, date, dist_name, dist_dir, dist_version, ident) } /* make distribution */ if (release.isabelle_archive.is_file) { progress.echo_warning("Release archive already exists: " + release.isabelle_archive) val archive_ident = Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val getsettings = Path.explode(release.dist_name + "/" + getsettings_file) execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings)) split_lines(File.read(tmp_dir + getsettings)) .collectFirst({ case ISABELLE_ID(ident) => ident }) .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive)) }) if (release.ident != archive_ident) { error("Mismatch of release identification " + release.ident + " vs. archive " + archive_ident) } } else { progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...") Isabelle_System.mkdirs(release.dist_dir) if (release.isabelle_dir.is_dir) error("Directory " + release.isabelle_dir + " already exists") progress.echo_warning("Retrieving Mercurial repository version " + release.ident) hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files") for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { (release.isabelle_dir + Path.explode(name)).file.delete } progress.echo_warning("Preparing distribution " + quote(release.dist_name)) patch_release(release, proper_release_name.isDefined && official_release) if (proper_release_name.isEmpty) make_announce(release) make_contrib(release.isabelle_dir) execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""") record_bundled_components(release.isabelle_dir) /* build tools and documentation */ val other_isabelle = release.other_isabelle(release.dist_dir) other_isabelle.init_settings( other_isabelle.init_components(base = components_base, catalogs = List("main"))) other_isabelle.resolve_components(echo = true) try { val export_classpath = "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check } catch { case ERROR(_) => error("Failed to build tools") } try { other_isabelle.bash( "./bin/isabelle build_doc -a -s -j " + parallel_jobs, echo = true).check } catch { case ERROR(_) => error("Failed to build documentation") } make_news(other_isabelle, release.dist_version) for (name <- List("Admin", "browser_info", "heaps")) { Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) } other_isabelle.cleanup() progress.echo_warning("Creating distribution archive " + release.isabelle_archive) def execute_dist_name(script: String): Unit = Isabelle_System.bash(script, cwd = release.dist_dir.file, env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check execute_dist_name(""" set -e chmod -R a+r "$DIST_NAME" chmod -R u+w "$DIST_NAME" chmod -R g=o "$DIST_NAME" find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w """) - execute_tar(release.dist_dir, tar_options + " -czf " + + execute_tar(release.dist_dir, "-czf " + File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name)) execute_dist_name(""" set -e mv "$DIST_NAME" "${DIST_NAME}-old" mkdir "$DIST_NAME" mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \ "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME" mkdir "$DIST_NAME/doc" mv "${DIST_NAME}-old/doc/"*.pdf \ "${DIST_NAME}-old/doc/"*.html \ "${DIST_NAME}-old/doc/"*.css \ "${DIST_NAME}-old/doc/fonts" \ "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc" rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle rm -rf "${DIST_NAME}-old" """) } /* make application bundles */ val bundle_infos = platform_families.map(release.bundle_info) for (bundle_info <- bundle_infos) { - val bundle = - (if (remote_mac.isEmpty) bundle_info.fallback else None) getOrElse bundle_info.main - val bundle_archive = release.dist_dir + Path.explode(bundle) + val bundle_archive = release.dist_dir + bundle_info.path if (bundle_archive.is_file && more_components.isEmpty) progress.echo_warning("Application bundle already exists: " + bundle_archive) else { val isabelle_name = release.dist_name val platform = bundle_info.platform - progress.echo("\nApplication bundle for " + platform + ": " + bundle_archive) + progress.echo("\nApplication bundle for " + platform) Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { // release archive execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive)) val other_isabelle = release.other_isabelle(tmp_dir) val isabelle_target = other_isabelle.isabelle_home // bundled components progress.echo("Bundled components:") val contrib_dir = Components.contrib(isabelle_target) val (bundled_components, jdk_component) = get_bundled_components(isabelle_target, platform) Components.resolve(other_isabelle.components_base(components_base), bundled_components, target_dir = Some(contrib_dir), progress = progress) val more_components_names = more_components.map(Components.unpack(contrib_dir, _, progress = progress)) Components.purge(contrib_dir, platform) activate_components(isabelle_target, platform, more_components_names) // Java parameters val java_options_title = "# Java runtime options" val java_options: List[String] = (for { variable <- List( "ISABELLE_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_SYSTEM_OPTIONS", "JEDIT_JAVA_OPTIONS") opt <- Word.explode(other_isabelle.getenv(variable)) } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name) val classpath: List[Path] = { val base = isabelle_target.absolute Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path => { val abs_path = path.absolute File.relative_path(base, abs_path) match { case Some(rel_path) => rel_path case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path) } }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar")) } val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props") - // platform-specific setup (inside archive) + // application bundling platform match { case Platform.Family.linux => File.write(isabelle_target + Path.explode(isabelle_name + ".options"), terminate_lines(java_options_title :: java_options)) val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run") File.write(isabelle_run, File.read(Path.explode("~~/Admin/Linux/Isabelle.run")) .replaceAllLiterally("{CLASSPATH}", classpath.map("$ISABELLE_HOME/" + _).mkString(":")) .replaceAllLiterally("/jdk/", "/" + jdk_component + "/")) File.executable(isabelle_run) val linux_app = isabelle_target + Path.explode("contrib/linux_app") File.move(linux_app + Path.explode("Isabelle"), isabelle_target + Path.explode(isabelle_name)) Isabelle_System.rm_tree(linux_app) + val archive_name = isabelle_name + "_linux.tar.gz" + progress.echo("Packaging " + archive_name + " ...") + execute_tar(tmp_dir, + "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + + Bash.string(isabelle_name)) + + case Platform.Family.macos => - File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir) File.write(isabelle_target + jedit_props, File.read(isabelle_target + jedit_props) .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel") .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d") .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar=")) - case Platform.Family.windows => - val app_template = Path.explode("~~/Admin/Windows/launch4j") - val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") - - File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) - - File.write(isabelle_target + jedit_props, - File.read(isabelle_target + jedit_props) - .replaceAll("lookAndFeel=.*", - "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel") - .replaceAll("foldPainter=.*", "foldPainter=Square")) - - File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), - (java_options_title :: java_options).map(_ + "\r\n").mkString) - - val isabelle_xml = Path.explode("isabelle.xml") - val isabelle_exe = Path.explode(isabelle_name + ".exe") - - File.write(tmp_dir + isabelle_xml, - File.read(app_template + isabelle_xml) - .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) - .replaceAllLiterally("{OUTFILE}", - File.platform_path(isabelle_target + isabelle_exe)) - .replaceAllLiterally("{ICON}", - File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) - .replaceAllLiterally("{SPLASH}", - File.platform_path(app_template + Path.explode("isabelle.bmp"))) - .replaceAllLiterally("{CLASSPATH}", - cat_lines(classpath.map(cp => - " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + ""))) - .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\")) - - execute(tmp_dir, - "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml") - - File.copy(app_template + Path.explode("manifest.xml"), - isabelle_target + isabelle_exe.ext("manifest")) - - - File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target) - - val cygwin_mirror = - File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror")) - val cygwin_bat = Path.explode("Cygwin-Setup.bat") - File.write(isabelle_target + cygwin_bat, - File.read(cygwin_template + cygwin_bat) - .replaceAllLiterally("{MIRROR}", cygwin_mirror)) - File.executable(isabelle_target + cygwin_bat) - - for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) { - val path = Path.explode(name) - File.copy(cygwin_template + path, - isabelle_target + Path.explode("contrib/cygwin") + path) - } - - execute(isabelle_target, - """find . -type f -not -name "*.exe" -not -name "*.dll" """ + - (if (Platform.is_macos) "-perm +100" else "-executable") + - " -print0 > contrib/cygwin/isabelle/executables") - - execute(isabelle_target, - """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ + - """> contrib/cygwin/isabelle/symlinks""") - - execute(isabelle_target, """find . -type l -exec rm "{}" ";" """) + // MacOS application bundle - File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") - } - - - // archive - - val archive_name = isabelle_name + "_" + platform + ".tar.gz" - progress.echo("Packaging " + archive_name + " ...") - execute_tar(tmp_dir, - "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + - Bash.string(isabelle_name)) - + File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir) - // platform-specific application (outside archive) - - progress.echo("Application for " + platform + " ...") - - platform match { - case Platform.Family.linux => - File.link( - Path.explode(isabelle_name + "_linux.tar.gz"), - release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"), - force = true) - - case Platform.Family.macos => - val dmg_dir = tmp_dir + Path.explode("macos_app/dmg") - val app_dir = dmg_dir + Path.explode(isabelle_name + ".app") - File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir) + val isabelle_app = Path.explode(isabelle_name + ".app") + val app_dir = tmp_dir + isabelle_app + File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir) val app_contents = app_dir + Path.explode("Contents") val app_resources = app_contents + Path.explode("Resources") File.move(tmp_dir + Path.explode(isabelle_name), app_resources) File.write(app_contents + Path.explode("Info.plist"), File.read(Path.explode("~~/Admin/MacOS/Info.plist")) .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) .replaceAllLiterally("{JAVA_OPTIONS}", terminate_lines(java_options.map(opt => "" + opt + "")))) for (cp <- classpath) { File.link( Path.explode("../Resources/" + isabelle_name + "/") + cp, app_contents + Path.explode("Java"), force = true) } File.link( Path.explode("../Resources/" + isabelle_name + "/contrib/" + jdk_component + "/x86_64-darwin"), app_contents + Path.explode("PlugIns/bundled.jdk"), force = true) File.link( Path.explode("../../Info.plist"), app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"), force = true) File.link( Path.explode("Contents/Resources/" + isabelle_name), app_dir + Path.explode("Isabelle"), force = true) - val dmg = Path.explode(isabelle_name + ".dmg") - (release.dist_dir + dmg).file.delete - - val dmg_archive = Path.explode(isabelle_name + "_dmg.tar.gz") - execute_tar(dmg_dir, "-czf " + File.bash_path(release.dist_dir + dmg_archive) + " .") - remote_mac match { - case SSH.Target(user, host) => - progress.echo("Building dmg on " + quote(host) + " ...") - using(SSH.open_session(options, host = host, user = user))(ssh => - { - ssh.with_tmp_dir(remote_dir => - { - val cd = "cd " + ssh.bash_path(remote_dir) + "; " - ssh.write_file(remote_dir + dmg_archive, release.dist_dir + dmg_archive) - ssh.execute( - cd + "mkdir root && tar -C root -xzf " + ssh.bash_path(dmg_archive)).check - ssh.execute( - cd + "hdiutil create -srcfolder root -volname Isabelle " + - ssh.bash_path(dmg)).check - ssh.read_file(remote_dir + dmg, release.dist_dir + dmg) - }) - }) - case _ => + // application archive + + val archive_name = isabelle_name + "_macos.tar.gz" + progress.echo("Packaging " + archive_name + " ...") + execute_tar(tmp_dir, + "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + + File.bash_path(isabelle_app)) + + + case Platform.Family.windows => + File.write(isabelle_target + jedit_props, + File.read(isabelle_target + jedit_props) + .replaceAll("lookAndFeel=.*", + "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel") + .replaceAll("foldPainter=.*", "foldPainter=Square")) + + + // application launcher + + File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) + + val app_template = Path.explode("~~/Admin/Windows/launch4j") + + File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), + (java_options_title :: java_options).map(_ + "\r\n").mkString) + + val isabelle_xml = Path.explode("isabelle.xml") + val isabelle_exe = Path.explode(isabelle_name + ".exe") + + File.write(tmp_dir + isabelle_xml, + File.read(app_template + isabelle_xml) + .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) + .replaceAllLiterally("{OUTFILE}", + File.platform_path(isabelle_target + isabelle_exe)) + .replaceAllLiterally("{ICON}", + File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) + .replaceAllLiterally("{SPLASH}", + File.platform_path(app_template + Path.explode("isabelle.bmp"))) + .replaceAllLiterally("{CLASSPATH}", + cat_lines(classpath.map(cp => + " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + ""))) + .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\")) + + execute(tmp_dir, + "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml") + + File.copy(app_template + Path.explode("manifest.xml"), + isabelle_target + isabelle_exe.ext("manifest")) + + + // Cygwin setup + + val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") + + File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target) + + val cygwin_mirror = + File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror")) + + val cygwin_bat = Path.explode("Cygwin-Setup.bat") + File.write(isabelle_target + cygwin_bat, + File.read(cygwin_template + cygwin_bat) + .replaceAllLiterally("{MIRROR}", cygwin_mirror)) + File.executable(isabelle_target + cygwin_bat) + + for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) { + val path = Path.explode(name) + File.copy(cygwin_template + path, + isabelle_target + Path.explode("contrib/cygwin") + path) } - case Platform.Family.windows => + execute(isabelle_target, + """find . -type f -not -name "*.exe" -not -name "*.dll" """ + + (if (Platform.is_macos) "-perm +100" else "-executable") + + " -print0 > contrib/cygwin/isabelle/executables") + + execute(isabelle_target, + """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ + + """> contrib/cygwin/isabelle/symlinks""") + + execute(isabelle_target, """find . -type l -exec rm "{}" ";" """) + + File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") + + + // executable archive (self-extracting 7z) + val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z") exe_archive.file.delete execute(tmp_dir, "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name)) if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive) - val isabelle_exe = Path.explode(isabelle_name + ".exe") val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx") val sfx_txt = File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")). replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) Bytes.write(release.dist_dir + isabelle_exe, Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive)) File.executable(release.dist_dir + isabelle_exe) } }) progress.echo("DONE") } } /* minimal website */ for (dir <- website) { val website_platform_bundles = for { bundle_info <- bundle_infos - bundle <- bundle_info.names.find(name => (release.dist_dir + Path.explode(name)).is_file) - } yield (bundle, bundle_info) + if (release.dist_dir + bundle_info.path).is_file + } yield (bundle_info.name, bundle_info) val afp_link = HTML.link(AFP.repos_source + "/commits/" + afp_rev, HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", List(HTML.title(release.dist_name)), List( HTML.chapter(release.dist_name + " (" + release.ident + ")"), HTML.itemize( website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) }))) ::: (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))) for ((bundle, _) <- website_platform_bundles) File.copy(release.dist_dir + Path.explode(bundle), dir) } /* HTML library */ if (build_library) { if (release.isabelle_library_archive.is_file) { progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive) } else { Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val bundle = release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz") execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) val other_isabelle = release.other_isabelle(tmp_dir) Isabelle_System.mkdirs(other_isabelle.etc) File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") other_isabelle.bash("bin/isabelle build -j " + parallel_jobs + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -s -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name)) execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name)) - execute_tar(tmp_dir, - tar_options + " -czf " + File.bash_path(release.isabelle_library_archive) + + execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) + " " + Bash.string(release.dist_name + "/browser_info")) }) } } release } /** command line entry point **/ def main(args: Array[String]) { Command_Line.tool0 { var afp_rev = "" var components_base: Option[Path] = None - var remote_mac = "" var official_release = false var proper_release_name: Option[String] = None var website: Option[Path] = None var more_components: List[Path] = Nil var parallel_jobs = 1 var build_library = false var options = Options.init() var platform_families = default_platform_families var rev = "" val getopts = Getopts(""" Usage: Admin/build_release [OPTIONS] BASE_DIR Options are: -A REV corresponding AFP changeset id -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib) - -M USER@HOST remote Mac OS X for dmg build -O official release (not release-candidate) -R RELEASE proper release with name -W WEBSITE produce minimal website in given directory -c ARCHIVE clean bundling with additional component .tar.gz archive -j INT maximum number of parallel jobs (default 1) -l build library -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) -r REV Mercurial changeset id (default: RELEASE or tip) Build Isabelle release in base directory, using the local repository clone. """, "A:" -> (arg => afp_rev = arg), "C:" -> (arg => components_base = Some(Path.explode(arg))), - "M:" -> (arg => remote_mac = arg), "O" -> (_ => official_release = true), "R:" -> (arg => proper_release_name = Some(arg)), "W:" -> (arg => website = Some(Path.explode(arg))), "c:" -> (arg => { val path = Path.explode(arg) Components.Archive.get_name(path.file_name) more_components = more_components ::: List(path) }), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), "r:" -> (arg => rev = arg)) val more_args = getopts(args) val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } val progress = new Console_Progress() if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) error("Building for windows requires 7z") build_release(Path.explode(base_dir), options, components_base = components_base, progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release, proper_release_name = proper_release_name, website = website, platform_families = if (platform_families.isEmpty) default_platform_families else platform_families, more_components = more_components, build_library = build_library, - parallel_jobs = parallel_jobs, remote_mac = remote_mac) + parallel_jobs = parallel_jobs) } } } diff --git a/src/Pure/System/components.scala b/src/Pure/Admin/components.scala rename from src/Pure/System/components.scala rename to src/Pure/Admin/components.scala --- a/src/Pure/System/components.scala +++ b/src/Pure/Admin/components.scala @@ -1,91 +1,293 @@ /* Title: Pure/Admin/components.scala Author: Makarius Isabelle system components. */ package isabelle import java.io.{File => JFile} object Components { /* archive name */ object Archive { val suffix: String = ".tar.gz" - def apply(name: String): String = name + suffix - def unapply(archive: String): Option[String] = Library.try_unsuffix(suffix, archive) + + def apply(name: String): String = + if (name == "") error("Bad component name: " + quote(name)) + else name + suffix + + def unapply(archive: String): Option[String] = + { + for { + name0 <- Library.try_unsuffix(suffix, archive) + name <- proper_string(name0) + } yield name + } + def get_name(archive: String): String = unapply(archive) getOrElse error("Bad component archive name (expecting .tar.gz): " + quote(archive)) } /* component collections */ def admin(dir: Path): Path = dir + Path.explode("Admin/components") def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String = { val name = Archive.get_name(archive.file_name) progress.echo("Unpacking " + name) - Isabelle_System.gnutar( - "-C " + File.bash_path(dir) + " -xzf " + File.bash_path(archive.absolute)).check + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check name } def resolve(base_dir: Path, names: List[String], target_dir: Option[Path] = None, progress: Progress = No_Progress) { Isabelle_System.mkdirs(base_dir) for (name <- names) { val archive_name = Archive(name) val archive = base_dir + Path.explode(archive_name) if (!archive.is_file) { val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name progress.echo("Getting " + remote) Bytes.write(archive, Url.read_bytes(Url(remote))) } unpack(target_dir getOrElse base_dir, archive, progress = progress) } } def purge(dir: Path, platform: Platform.Family.Value) { def purge_platforms(platforms: String*): Set[String] = platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin" val purge_set = platform match { case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows") case Platform.Family.macos => purge_platforms("linux", "cygwin", "windows") case Platform.Family.windows => purge_platforms("linux", "darwin") } File.find_files(dir.file, (file: JFile) => file.isDirectory && purge_set(file.getName), include_dirs = true).foreach(Isabelle_System.rm_tree) } /* component directory content */ - def settings(dir: Path): Path = dir + Path.explode("etc/settings") - def components(dir: Path): Path = dir + Path.explode("etc/components") + def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings") + def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components") def check_dir(dir: Path): Boolean = settings(dir).is_file || components(dir).is_file def read_components(dir: Path): List[String] = split_lines(File.read(components(dir))).filter(_.nonEmpty) def write_components(dir: Path, lines: List[String]): Unit = File.write(components(dir), terminate_lines(lines)) + + + /* component repository content */ + + val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") + + sealed case class SHA1_Digest(sha1: String, file_name: String) + { + override def toString: String = sha1 + " " + file_name + } + + def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = + (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => + Word.explode(line) match { + case Nil => None + case List(sha1, name) => Some(SHA1_Digest(sha1, name)) + case _ => error("Bad components.sha1 entry: " + quote(line)) + }) + + def write_components_sha1(entries: List[SHA1_Digest]) = + File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n")) + + + + /** build and publish components **/ + + def build_components( + options: Options, + components: List[Path], + progress: Progress = No_Progress, + publish: Boolean = false, + force: Boolean = false, + update_components_sha1: Boolean = false) + { + val archives: List[Path] = + for (path <- components) yield { + path.file_name match { + case Archive(_) => path + case name => + if (!path.is_dir) error("Bad component directory: " + path) + else if (!check_dir(path)) { + error("Malformed component directory: " + path + + "\n (requires " + settings() + " or " + Components.components() + ")") + } + else { + val component_path = path.expand + val archive_dir = component_path.dir + val archive_name = Archive(name) + + val archive = archive_dir + Path.explode(archive_name) + if (archive.is_file && !force) { + error("Component archive already exists: " + archive) + } + + progress.echo("Packaging " + archive_name + " ...") + Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), + dir = archive_dir).check + + archive + } + } + } + + if ((publish && archives.nonEmpty) || update_components_sha1) { + options.string("isabelle_components_server") match { + case SSH.Target(user, host) => + using(SSH.open_session(options, host = host, user = user))(ssh => + { + val components_dir = Path.explode(options.string("isabelle_components_dir")) + val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) + + for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { + error("Bad remote directory: " + dir) + } + + if (publish) { + for (archive <- archives) { + val archive_name = archive.file_name + val name = Archive.get_name(archive_name) + val remote_component = components_dir + archive.base + val remote_contrib = contrib_dir + Path.explode(name) + + // component archive + if (ssh.is_file(remote_component) && !force) { + error("Remote component archive already exists: " + remote_component) + } + progress.echo("Uploading " + archive_name) + ssh.write_file(remote_component, archive) + + // contrib directory + val is_standard_component = + Isabelle_System.with_tmp_dir("component")(tmp_dir => + { + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check + check_dir(tmp_dir + Path.explode(name)) + }) + if (is_standard_component) { + if (ssh.is_dir(remote_contrib)) { + if (force) ssh.rm_tree(remote_contrib) + else error("Remote component directory already exists: " + remote_contrib) + } + progress.echo("Unpacking remote " + archive_name) + ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + + ssh.bash_path(remote_component)).check + } + else { + progress.echo_warning("No unpacking of non-standard component: " + archive_name) + } + } + } + + // remote SHA1 digests + if (update_components_sha1) { + val lines = + for { + entry <- ssh.read_dir(components_dir) + if entry.is_file && entry.name.endsWith(Archive.suffix) + } + yield { + progress.echo("Digesting remote " + entry.name) + Library.trim_line( + ssh.execute("cd " + ssh.bash_path(components_dir) + + "; sha1sum " + Bash.string(entry.name)).check.out) + } + write_components_sha1(read_components_sha1(lines)) + } + }) + case s => error("Bad isabelle_components_server: " + quote(s)) + } + } + + // local SHA1 digests + { + val new_entries = + for (archive <- archives) + yield { + val file_name = archive.file_name + progress.echo("Digesting local " + file_name) + val sha1 = SHA1.digest(archive).rep + SHA1_Digest(sha1, file_name) + } + val new_names = new_entries.map(_.file_name).toSet + + write_components_sha1( + new_entries ::: + read_components_sha1().filterNot(entry => new_names.contains(entry.file_name))) + } + } + + + /* Isabelle tool wrapper */ + + private val relevant_options = + List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") + + val isabelle_tool = + Isabelle_Tool("build_components", "build and publish Isabelle components", args => + { + var publish = false + var update_components_sha1 = false + var force = false + var options = Options.init() + + def show_options: String = + cat_lines(relevant_options.map(name => options.options(name).print)) + + val getopts = Getopts(""" +Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... + + Options are: + -P publish on SSH server (see options below) + -f force: overwrite existing component archives and directories + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -u update all SHA1 keys in Isabelle repository Admin/components + + Build and publish Isabelle components as .tar.gz archives on SSH server, + depending on system options: + +""" + Library.prefix_lines(" ", show_options) + "\n", + "P" -> (_ => publish = true), + "f" -> (_ => force = true), + "o:" -> (arg => options = options + arg), + "u" -> (_ => update_components_sha1 = true)) + + val more_args = getopts(args) + if (more_args.isEmpty && !update_components_sha1) getopts.usage() + + val progress = new Console_Progress + + build_components(options, more_args.map(Path.explode), progress = progress, + publish = publish, force = force, update_components_sha1 = update_components_sha1) + }) } diff --git a/src/Pure/Admin/isabelle_cronjob.scala b/src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala +++ b/src/Pure/Admin/isabelle_cronjob.scala @@ -1,587 +1,586 @@ /* Title: Pure/Admin/isabelle_cronjob.scala Author: Makarius Main entry point for administrative cronjob at TUM. */ package isabelle import java.nio.file.Files import scala.annotation.tailrec import scala.collection.mutable object Isabelle_Cronjob { /* global resources: owned by main cronjob */ val backup = "lxbroy10:cronjob" val main_dir = Path.explode("~/cronjob") val main_state_file = main_dir + Path.explode("run/main.state") val current_log = main_dir + Path.explode("run/main.log") // owned by log service val cumulative_log = main_dir + Path.explode("log/main.log") // owned by log service val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle" val isabelle_repos = main_dir + Path.explode("isabelle") val afp_repos = main_dir + Path.explode("AFP") val build_log_dirs = List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log")) /** logger tasks **/ sealed case class Logger_Task(name: String = "", body: Logger => Unit) /* init and exit */ def get_rev(): String = Mercurial.repository(isabelle_repos).id() def get_afp_rev(): String = Mercurial.repository(afp_repos).id() val init = Logger_Task("init", logger => { Isabelle_Devel.make_index() Mercurial.setup_repository(isabelle_repos_source, isabelle_repos) Mercurial.setup_repository(AFP.repos_source, afp_repos) File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date), Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev()))) Isabelle_System.bash( """rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ + Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check if (!Isabelle_Devel.cronjob_log.is_file) Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath) }) val exit = Logger_Task("exit", logger => { Isabelle_System.bash( "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.") .check }) /* build release */ val build_release = Logger_Task("build_release", logger => { - Isabelle_Devel.release_snapshot(logger.options, - rev = get_rev(), afp_rev = get_afp_rev(), remote_mac = "macbroy30") + Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev()) }) /* integrity test of build_history vs. build_history_base */ val build_history_base = Logger_Task("build_history_base", logger => { using(logger.ssh_context.open_session("lxbroy10"))(ssh => { val results = Build_History.remote_build_history(ssh, isabelle_repos, isabelle_repos.ext("build_history_base"), isabelle_identifier = "cronjob_build_history", self_update = true, rev = "build_history_base", options = "-f", args = "HOL") for ((log_name, bytes) <- results) { Bytes.write(logger.log_dir + Path.explode(log_name), bytes) } }) }) /* remote build_history */ sealed case class Item( known: Boolean, isabelle_version: String, afp_version: Option[String], pull_date: Date) { def unknown: Boolean = !known def versions: (String, Option[String]) = (isabelle_version, afp_version) def known_versions(rev: String, afp_rev: Option[String]): Boolean = known && rev != "" && isabelle_version == rev && (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev.get) } def recent_items(db: SQL.Database, days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] = { val afp = afp_rev.isDefined val select = Build_Log.Data.select_recent_versions( days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql) db.using_statement(select)(stmt => stmt.execute_query().iterator(res => { val known = res.bool(Build_Log.Data.known) val isabelle_version = res.string(Build_Log.Prop.isabelle_version) val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None val pull_date = res.date(Build_Log.Data.pull_date(afp)) Item(known, isabelle_version, afp_version, pull_date) }).toList) } def unknown_runs(items: List[Item]): List[List[Item]] = { val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known)) if (run.nonEmpty) run :: unknown_runs(rest) else Nil } sealed case class Remote_Build( description: String, host: String, user: String = "", port: Int = 0, ssh_host: String = "", ssh_permissive: Boolean = false, proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, self_update: Boolean = false, historic: Boolean = false, history: Int = 0, history_base: String = "build_history_base", options: String = "", args: String = "", afp: Boolean = false, slow: Boolean = false, more_hosts: List[String] = Nil, detect: SQL.Source = "", active: Boolean = true) { def ssh_session(context: SSH.Context): SSH.Session = context.open_session(host = proper_string(ssh_host) getOrElse host, user = user, port = port, proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, permissive = ssh_permissive) def sql: SQL.Source = Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " + SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) + (if (detect == "") "" else " AND " + SQL.enclose(detect)) def profile: Build_Status.Profile = Build_Status.Profile(description, history = history, afp = afp, slow = slow, sql = sql) def pick( options: Options, rev: String = "", filter: Item => Boolean = _ => true): Option[(String, Option[String])] = { val afp_rev = if (afp) Some(get_afp_rev()) else None val store = Build_Log.store(options) using(store.open_database())(db => { def pick_days(days: Int, gap: Int): Option[(String, Option[String])] = { val items = recent_items(db, days, rev, afp_rev, sql).filter(filter) def runs = unknown_runs(items).filter(run => run.length >= gap) if (historic || items.exists(_.known_versions(rev, afp_rev))) { val longest_run = (List.empty[Item] /: runs)({ case (item1, item2) => if (item1.length >= item2.length) item1 else item2 }) if (longest_run.isEmpty) None else Some(longest_run(longest_run.length / 2).versions) } else if (rev != "") Some((rev, afp_rev)) else runs.flatten.headOption.map(_.versions) } pick_days(options.int("build_log_history") max history, 2) orElse pick_days(200, 5) orElse pick_days(2000, 1) }) } } val remote_builds_old: List[Remote_Build] = List( Remote_Build("AFP", "lxbroy7", args = "-N -X slow", afp = true, detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", history_base = "37074e22e8be", options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-N -g timing", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7") + " AND " + Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")), Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-N -g timing", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2", history_base = "37074e22e8be", options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-a", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")), Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-a", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("Poly/ML test", "lxbroy8", options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'", args = "-N -g timing", detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")), Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start + " < date '2017-03-03'")) val remote_builds1: List[List[Remote_Build]] = { List( List(Remote_Build("Linux A", "lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")), List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90, options = "-m32 -B -M1x2,2 -t Benchmarks" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=sml -e ISABELLE_SWIPL=swipl", args = "-N -a -d '~~/src/Benchmarks'", detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))), List( Remote_Build("Mac OS X", "macbroy2", options = "-m32 -M8" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=/mnt/nfsbroy/home/smlnj/bin/sml", args = "-a", detect = Build_Log.Prop.build_tags.undefined, history_base = "2c0f24e927dd"), Remote_Build("Mac OS X, quick_and_dirty", "macbroy2", options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty", detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"), history_base = "2c0f24e927dd"), Remote_Build("Mac OS X, skip_proofs", "macbroy2", options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs", detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"), history_base = "2c0f24e927dd")), List( Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a", detect = Build_Log.Prop.build_start + " > date '2017-03-03'")), List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")), List(Remote_Build("Mac OS X 10.14 High Sierra", "lapbroy68", self_update = true, options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true -e ISABELLE_OCAML_SETUP=true", args = "-a -d '~~/src/Benchmarks'")), List(Remote_Build("Mac OS X 10.14 Mojave", "lapnipkow3", self_update = true, options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -e ISABELLE_OCAML_SETUP=true", args = "-a -d '~~/src/Benchmarks'")), List( Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, options = "-m32 -M4" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" + " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")), Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, options = "-m64 -M4" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" + " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))) ) ::: { for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) } yield { List(Remote_Build("AFP", host = hosts.head, more_hosts = hosts.tail, options = "-m32 -M1x2 -t AFP -P" + n + " -e ISABELLE_GHC=ghc" + " -e ISABELLE_MLTON=mlton" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" + " -e ISABELLE_SMLNJ=/home/smlnj/bin/sml", args = "-N -X slow", afp = true, detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))) } } } val remote_builds2: List[List[Remote_Build]] = List( List( Remote_Build("AFP slow", "lrzcloud1", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", ssh_host = "10.155.208.96", ssh_permissive = true, options = "-m64 -M6 -U30000 -s10 -t AFP", args = "-g slow", afp = true, slow = true, detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))) def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build) : Logger_Task = { val task_name = "build_history-" + r.host Logger_Task(task_name, logger => { using(r.ssh_session(logger.ssh_context))(ssh => { val results = Build_History.remote_build_history(ssh, isabelle_repos, isabelle_repos.ext(r.host), isabelle_identifier = "cronjob_build_history", self_update = r.self_update, rev = rev, afp_rev = afp_rev, options = " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) + " -f -h " + Bash.string(r.host) + " " + r.options, args = "-o timeout=10800 " + r.args) for ((log_name, bytes) <- results) { logger.log(Date.now(), log_name) Bytes.write(logger.log_dir + Path.explode(log_name), bytes) } }) }) } val build_status_profiles: List[Build_Status.Profile] = (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile) /** task logging **/ object Log_Service { def apply(options: Options, progress: Progress = No_Progress): Log_Service = new Log_Service(SSH.init_context(options), progress) } class Log_Service private(val ssh_context: SSH.Context, progress: Progress) { current_log.file.delete private val thread: Consumer_Thread[String] = Consumer_Thread.fork("cronjob: logger", daemon = true)( consume = (text: String) => { // critical File.append(current_log, text + "\n") File.append(cumulative_log, text + "\n") progress.echo(text) true }) def shutdown() { thread.shutdown() } val hostname = Isabelle_System.hostname() def log(date: Date, task_name: String, msg: String): Unit = if (task_name != "") thread.send( "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg) def start_logger(start_date: Date, task_name: String): Logger = new Logger(this, start_date, task_name) def run_task(start_date: Date, task: Logger_Task) { val logger = start_logger(start_date, task.name) val res = Exn.capture { task.body(logger) } val end_date = Date.now() val err = res match { case Exn.Res(_) => None case Exn.Exn(exn) => Output.writeln("Exception trace for " + quote(task.name) + ":") exn.printStackTrace() val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception" Some(first_line) } logger.log_end(end_date, err) } def fork_task(start_date: Date, task: Logger_Task): Task = new Task(task.name, run_task(start_date, task)) } class Logger private[Isabelle_Cronjob]( val log_service: Log_Service, val start_date: Date, val task_name: String) { def ssh_context: SSH.Context = log_service.ssh_context def options: Options = ssh_context.options def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg) def log_end(end_date: Date, err: Option[String]) { val elapsed_time = end_date.time - start_date.time val msg = (if (err.isEmpty) "finished" else "ERROR " + err.get) + (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)") log(end_date, msg) } val log_dir: Path = main_dir + Build_Log.log_subdir(start_date) Isabelle_System.mkdirs(log_dir) log(start_date, "started") } class Task private[Isabelle_Cronjob](name: String, body: => Unit) { private val future: Future[Unit] = Future.thread("cronjob: " + name) { body } def is_finished: Boolean = future.is_finished } /** cronjob **/ def cronjob(progress: Progress, exclude_task: Set[String]) { /* soft lock */ val still_running = try { Some(File.read(main_state_file)) } catch { case ERROR(_) => None } still_running match { case None | Some("") => case Some(running) => error("Isabelle cronjob appears to be still running: " + running) } /* log service */ val log_service = Log_Service(Options.init(), progress = progress) def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) } def run_now(task: Logger_Task) { run(Date.now(), task) } /* structured tasks */ def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "") run_now(task)) def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => { @tailrec def join(running: List[Task]) { running.partition(_.is_finished) match { case (Nil, Nil) => case (Nil, _ :: _) => Thread.sleep(500); join(running) case (_ :: _, remaining) => join(remaining) } } val start_date = Date.now() val running = for (task <- tasks if !exclude_task(task.name)) yield log_service.fork_task(start_date, task) join(running) }) /* repository structure */ val hg = Mercurial.repository(isabelle_repos) val hg_graph = hg.graph() def history_base_filter(r: Remote_Build): Item => Boolean = { val base_rev = hg.id(r.history_base) val nodes = hg_graph.all_succs(List(base_rev)).toSet (item: Item) => nodes(item.isabelle_version) } /* main */ val main_start_date = Date.now() File.write(main_state_file, main_start_date + " " + log_service.hostname) run(main_start_date, Logger_Task("isabelle_cronjob", logger => run_now( SEQ(List( init, build_history_base, PAR( build_release :: List(remote_builds1, remote_builds2).map(remote_builds => SEQ(List( PAR(remote_builds.map(_.filter(_.active)).map(seq => SEQ( for { (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex) (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r)) } yield remote_build_history(rev, afp_rev, i, r)))), Logger_Task("jenkins_logs", _ => Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)), Logger_Task("build_log_database", logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)), Logger_Task("build_status", logger => Isabelle_Devel.build_status(logger.options)))))), exit))))) log_service.shutdown() main_state_file.file.delete } /** command line entry point **/ def main(args: Array[String]) { Command_Line.tool0 { var force = false var verbose = false var exclude_task = Set.empty[String] val getopts = Getopts(""" Usage: Admin/cronjob/main [OPTIONS] Options are: -f apply force to do anything -v verbose -x NAME exclude tasks with this name """, "f" -> (_ => force = true), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_task += arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = if (verbose) new Console_Progress() else No_Progress if (force) cronjob(progress, exclude_task) else error("Need to apply force to do anything") } } } diff --git a/src/Pure/Admin/isabelle_devel.scala b/src/Pure/Admin/isabelle_devel.scala --- a/src/Pure/Admin/isabelle_devel.scala +++ b/src/Pure/Admin/isabelle_devel.scala @@ -1,91 +1,90 @@ /* Title: Pure/Admin/isabelle_devel.scala Author: Makarius Website for Isabelle development resources. */ package isabelle object Isabelle_Devel { val RELEASE_SNAPSHOT = "release_snapshot" val BUILD_LOG_DB = "build_log.db" val BUILD_STATUS = "build_status" val CRONJOB_LOG = "cronjob-main.log" val root = Path.explode("~/html-data/devel") val cronjob_log = root + Path.basic(CRONJOB_LOG) /* index */ def make_index() { val header = "Isabelle Development Resources" HTML.write_document(root, "index.html", List(HTML.title(header)), List(HTML.chapter(header), HTML.itemize( List( HTML.text("Isabelle nightly ") ::: List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) ::: HTML.text(" (for all platforms)"), HTML.text("Cronjob ") ::: List(HTML.link(CRONJOB_LOG, HTML.text("log file"))), HTML.text("Isabelle ") ::: List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) ::: HTML.text(" information"), HTML.text("Database with recent ") ::: List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) ::: HTML.text(" information (e.g. for ") ::: List(HTML.link("https://sqlitebrowser.org", List(HTML.code(HTML.text("sqlitebrowser"))))) ::: HTML.text(")"))))) } /* release snapshot */ def release_snapshot( options: Options, rev: String = "", afp_rev: String = "", - parallel_jobs: Int = 1, - remote_mac: String = "") + parallel_jobs: Int = 1) { Isabelle_System.with_tmp_dir("isadist")(base_dir => { Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT), website_dir => Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev, - parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir))) + parallel_jobs = parallel_jobs, website = Some(website_dir))) }) } /* maintain build_log database */ def build_log_database(options: Options, log_dirs: List[Path]) { val store = Build_Log.store(options) using(store.open_database())(db => { store.update_database(db, log_dirs) store.update_database(db, log_dirs, ml_statistics = true) store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB)) }) } /* present build status */ def build_status(options: Options) { Isabelle_System.update_directory(root + Path.explode(BUILD_STATUS), dir => Build_Status.build_status(options, target_dir = dir, ml_statistics = true)) } } diff --git a/src/Pure/General/file.ML b/src/Pure/General/file.ML --- a/src/Pure/General/file.ML +++ b/src/Pure/General/file.ML @@ -1,174 +1,174 @@ (* Title: Pure/General/file.ML Author: Makarius File-system operations. *) signature FILE = sig val standard_path: Path.T -> string val platform_path: Path.T -> string val bash_path: Path.T -> string val bash_paths: Path.T list -> string val full_path: Path.T -> Path.T -> Path.T val tmp_path: Path.T -> Path.T val exists: Path.T -> bool val rm: Path.T -> unit val is_dir: Path.T -> bool val is_file: Path.T -> bool val check_dir: Path.T -> Path.T val check_file: Path.T -> Path.T val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_dir: Path.T -> string list val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_lines: Path.T -> string list val read_pages: Path.T -> string list val read: Path.T -> string val write: Path.T -> string -> unit val append: Path.T -> string -> unit val generate: Path.T -> string -> unit val output: BinIO.outstream -> string -> unit val write_list: Path.T -> string list -> unit val append_list: Path.T -> string list -> unit val write_buffer: Path.T -> Buffer.T -> unit val eq: Path.T * Path.T -> bool end; structure File: FILE = struct (* system path representations *) val standard_path = Path.implode o Path.expand; val platform_path = ML_System.platform_path o standard_path; val bash_path = Bash_Syntax.string o standard_path; val bash_paths = Bash_Syntax.strings o map standard_path; (* full_path *) fun full_path dir path = let val path' = Path.expand path; val _ = Path.is_current path' andalso error "Bad file specification"; val path'' = Path.append dir path'; in if Path.is_absolute path'' then path'' else Path.append (Path.explode (ML_System.standard_path (OS.FileSys.getDir ()))) path'' end; (* tmp_path *) fun tmp_path path = Path.append (Path.variable "ISABELLE_TMP") (Path.base path); (* directory entries *) val exists = can OS.FileSys.modTime o platform_path; val rm = OS.FileSys.remove o platform_path; fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path)); fun is_dir path = exists path andalso test_dir path; fun is_file path = exists path andalso not (test_dir path); fun check_dir path = if is_dir path then path else error ("No such directory: " ^ Path.print (Path.expand path)); fun check_file path = if is_file path then path else error ("No such file: " ^ Path.print (Path.expand path)); (* open streams *) local fun with_file open_file close_file f path = let val file = open_file path in Exn.release (Exn.capture f file before close_file file) end; in fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path; fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path; fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path; fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path; end; (* directory content *) fun fold_dir f path a = check_dir path |> open_dir (fn stream => let fun read x = (case OS.FileSys.readDir stream of NONE => x | SOME entry => read (f entry x)); in read a end); -fun read_dir path = rev (fold_dir cons path []); +fun read_dir path = sort_strings (fold_dir cons path []); (* input *) (* scalable iterator: . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine . optional terminator at end-of-input *) fun fold_chunks terminator f path a = open_input (fn file => let fun read buf x = (case Byte.bytesToString (BinIO.input file) of "" => (case Buffer.content buf of "" => x | line => f line x) | input => (case String.fields (fn c => c = terminator) input of [rest] => read (Buffer.add rest buf) x | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x))) and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x | read_lines (line :: more) x = read_lines more (f line x); in read Buffer.empty a end) path; fun fold_lines f = fold_chunks #"\n" f; fun fold_pages f = fold_chunks #"\f" f; fun read_lines path = rev (fold_lines cons path []); fun read_pages path = rev (fold_pages cons path []); val read = open_input (Byte.bytesToString o BinIO.inputAll); (* output *) fun output file txt = BinIO.output (file, Byte.stringToBytes txt); fun output_list txts file = List.app (output file) txts; fun write_list path txts = open_output (output_list txts) path; fun append_list path txts = open_append (output_list txts) path; fun write path txt = write_list path [txt]; fun append path txt = append_list path [txt]; fun generate path txt = if try read path = SOME txt then () else write path txt; fun write_buffer path buf = open_output (Buffer.output buf) path; (* eq *) fun eq paths = (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of SOME ids => is_equal (OS.FileSys.compare ids) | NONE => false); end; diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala --- a/src/Pure/General/file.scala +++ b/src/Pure/General/file.scala @@ -1,343 +1,343 @@ /* Title: Pure/General/file.scala Author: Makarius File-system operations. */ package isabelle import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream, OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader, File => JFile, IOException} import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath, Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException} import java.nio.file.attribute.BasicFileAttributes import java.net.{URL, MalformedURLException} import java.util.zip.{GZIPInputStream, GZIPOutputStream} import java.util.regex.Pattern import java.util.EnumSet import org.tukaani.xz.{XZInputStream, XZOutputStream} import scala.collection.mutable import scala.util.matching.Regex object File { /* standard path (Cygwin or Posix) */ def standard_path(path: Path): String = path.expand.implode def standard_path(platform_path: String): String = if (Platform.is_windows) { val Platform_Root = new Regex("(?i)" + Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""") val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") platform_path.replace('/', '\\') match { case Platform_Root(rest) => "/" + rest.replace('\\', '/') case Drive(letter, rest) => "/cygdrive/" + Word.lowercase(letter) + (if (rest == "") "" else "/" + rest.replace('\\', '/')) case path => path.replace('\\', '/') } } else platform_path def standard_path(file: JFile): String = standard_path(file.getPath) def standard_url(name: String): String = try { val url = new URL(name) if (url.getProtocol == "file" && Url.is_wellformed_file(name)) standard_path(Url.parse_file(name)) else name } catch { case _: MalformedURLException => standard_path(name) } /* platform path (Windows or Posix) */ private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") private val Named_Root = new Regex("//+([^/]*)(.*)") def platform_path(standard_path: String): String = if (Platform.is_windows) { val result_path = new StringBuilder val rest = standard_path match { case Cygdrive(drive, rest) => result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) rest case Named_Root(root, rest) => result_path ++= JFile.separator result_path ++= JFile.separator result_path ++= root rest case path if path.startsWith("/") => result_path ++= Isabelle_System.cygwin_root() path case path => path } for (p <- space_explode('/', rest) if p != "") { val len = result_path.length if (len > 0 && result_path(len - 1) != JFile.separatorChar) result_path += JFile.separatorChar result_path ++= p } result_path.toString } else standard_path def platform_path(path: Path): String = platform_path(standard_path(path)) def platform_file(path: Path): JFile = new JFile(platform_path(path)) /* platform files */ def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile def absolute_name(file: JFile): String = absolute(file).getPath def canonical(file: JFile): JFile = file.getCanonicalFile def canonical_name(file: JFile): String = canonical(file).getPath def path(file: JFile): Path = Path.explode(standard_path(file)) def pwd(): Path = path(Path.current.absolute_file) /* relative paths */ def relative_path(base: Path, other: Path): Option[Path] = { val base_path = base.file.toPath val other_path = other.file.toPath if (other_path.startsWith(base_path)) Some(path(base_path.relativize(other_path).toFile)) else None } def rebase_path(base: Path, other: Path): Option[Path] = relative_path(base, other).map(base + _) /* bash path */ def bash_path(path: Path): String = Bash.string(standard_path(path)) def bash_path(file: JFile): String = Bash.string(standard_path(file)) /* directory entries */ def check_dir(path: Path): Path = if (path.is_dir) path else error("No such directory: " + path) def check_file(path: Path): Path = if (path.is_file) path else error("No such file: " + path) /* directory content */ def read_dir(dir: Path): List[String] = { if (!dir.is_dir) error("No such directory: " + dir.toString) val files = dir.file.listFiles if (files == null) Nil - else files.toList.map(_.getName) + else files.toList.map(_.getName).sorted } def find_files( start: JFile, pred: JFile => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false): List[JFile] = { val result = new mutable.ListBuffer[JFile] def check(file: JFile) { if (pred(file)) result += file } if (start.isFile) check(start) else if (start.isDirectory) { val options = if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS) else EnumSet.noneOf(classOf[FileVisitOption]) Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE, new SimpleFileVisitor[JPath] { override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult = { if (include_dirs) check(path.toFile) FileVisitResult.CONTINUE } override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult = { val file = path.toFile if (include_dirs || !file.isDirectory) check(file) FileVisitResult.CONTINUE } } ) } result.toList } /* read */ def read(file: JFile): String = Bytes.read(file).text def read(path: Path): String = read(path.file) def read_stream(reader: BufferedReader): String = { val output = new StringBuilder(100) var c = -1 while ({ c = reader.read; c != -1 }) output += c.toChar reader.close output.toString } def read_stream(stream: InputStream): String = read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset))) def read_gzip(file: JFile): String = read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_gzip(path: Path): String = read_gzip(path.file) def read_xz(file: JFile): String = read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_xz(path: Path): String = read_xz(path.file) /* read lines */ def read_lines(reader: BufferedReader, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] var line: String = null while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) { progress(line) result += line } reader.close result.toList } /* write */ def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream) { val stream = make_stream(new FileOutputStream(file)) using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text)) } def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s) def write(path: Path, text: CharSequence): Unit = write(path.file, text) def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s))) def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit = File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options)) def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options()) def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit = write_xz(path.file, text, options) def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options()) def write_backup(path: Path, text: CharSequence) { if (path.is_file) move(path, path.backup) write(path, text) } def write_backup2(path: Path, text: CharSequence) { if (path.is_file) move(path, path.backup2) write(path, text) } /* append */ def append(file: JFile, text: CharSequence): Unit = Files.write(file.toPath, UTF8.bytes(text.toString), StandardOpenOption.APPEND, StandardOpenOption.CREATE) def append(path: Path, text: CharSequence): Unit = append(path.file, text) /* eq */ def eq(file1: JFile, file2: JFile): Boolean = try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) } catch { case ERROR(_) => false } def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file) /* eq_content */ def eq_content(file1: JFile, file2: JFile): Boolean = if (eq(file1, file2)) true else if (file1.length != file2.length) false else Bytes.read(file1) == Bytes.read(file2) def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file) /* copy */ def copy(src: JFile, dst: JFile) { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!eq(src, target)) Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file) /* move */ def move(src: JFile, dst: JFile) { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file) /* symbolic link */ def link(src: Path, dst: Path, force: Boolean = false) { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => Cygwin.link(standard_path(src), target) case _: FileSystemException if Platform.is_windows => Cygwin.link(standard_path(src), target) } } /* permissions */ def executable(path: Path) { if (Platform.is_windows) Isabelle_System.bash("chmod a+x " + bash_path(path)).check else path.file.setExecutable(true, false) } } diff --git a/src/Pure/General/ssh.scala b/src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala +++ b/src/Pure/General/ssh.scala @@ -1,484 +1,484 @@ /* Title: Pure/General/ssh.scala Author: Makarius SSH client based on JSch (see also http://www.jcraft.com/jsch/examples). */ package isabelle import java.io.{InputStream, OutputStream, ByteArrayOutputStream} import scala.collection.{mutable, JavaConversions} import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException, OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS} object SSH { /* target machine: user@host syntax */ object Target { val Pattern = "^([^@]+)@(.+)$".r def parse(s: String): (String, String) = s match { case Pattern(user, host) => (user, host) case _ => ("", s) } def unapplySeq(s: String): Option[List[String]] = parse(s) match { case (_, "") => None case (user, host) => Some(List(user, host)) } } val default_port = 22 def make_port(port: Int): Int = if (port > 0) port else default_port def connect_timeout(options: Options): Int = options.seconds("ssh_connect_timeout").ms.toInt def alive_interval(options: Options): Int = options.seconds("ssh_alive_interval").ms.toInt def alive_count_max(options: Options): Int = options.int("ssh_alive_count_max") /* init context */ def init_context(options: Options): Context = { val config_dir = Path.explode(options.string("ssh_config_dir")) if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir) val jsch = new JSch val config_file = Path.explode(options.string("ssh_config_file")) if (config_file.is_file) jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) val known_hosts = config_dir + Path.explode("known_hosts") if (!known_hosts.is_file) known_hosts.file.createNewFile jsch.setKnownHosts(File.platform_path(known_hosts)) val identity_files = space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_)) for (identity_file <- identity_files if identity_file.is_file) jsch.addIdentity(File.platform_path(identity_file)) new Context(options, jsch) } def open_session(options: Options, host: String, user: String = "", port: Int = 0, proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, permissive: Boolean = false): Session = init_context(options).open_session(host = host, user = user, port = port, proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, permissive = permissive) class Context private[SSH](val options: Options, val jsch: JSch) { def update_options(new_options: Options): Context = new Context(new_options, jsch) def connect_session(host: String, user: String = "", port: Int = 0, host_key_permissive: Boolean = false, host_key_alias: String = "", on_close: () => Unit = () => ()): Session = { val session = jsch.getSession(proper_string(user) getOrElse null, host, make_port(port)) session.setUserInfo(No_User_Info) session.setServerAliveInterval(alive_interval(options)) session.setServerAliveCountMax(alive_count_max(options)) session.setConfig("MaxAuthTries", "3") if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no") if (host_key_alias != "") session.setHostKeyAlias(host_key_alias) if (options.bool("ssh_compression")) { session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") session.setConfig("compression_level", "9") } session.connect(connect_timeout(options)) new Session(options, session, on_close) } def open_session(host: String, user: String = "", port: Int = 0, proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, permissive: Boolean = false): Session = { if (proxy_host == "") connect_session(host = host, user = user, port = port) else { val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user) val fw = try { proxy.port_forwarding(remote_host = host, remote_port = make_port(port)) } catch { case exn: Throwable => proxy.close; throw exn } try { connect_session(host = fw.local_host, port = fw.local_port, host_key_permissive = permissive, host_key_alias = host, user = user, on_close = () => { fw.close; proxy.close }) } catch { case exn: Throwable => fw.close; proxy.close; throw exn } } } } /* logging */ def logging(verbose: Boolean = true, debug: Boolean = false) { JSch.setLogger(if (verbose) new Logger(debug) else null) } private class Logger(debug: Boolean) extends JSch_Logger { def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug def log(level: Int, msg: String) { level match { case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) case JSch_Logger.WARN => Output.warning(msg) case _ => Output.writeln(msg) } } } /* user info */ object No_User_Info extends UserInfo { def getPassphrase: String = null def getPassword: String = null def promptPassword(msg: String): Boolean = false def promptPassphrase(msg: String): Boolean = false def promptYesNo(msg: String): Boolean = false def showMessage(msg: String): Unit = Output.writeln(msg) } /* port forwarding */ object Port_Forwarding { def open(ssh: Session, ssh_close: Boolean, local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding = { val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port) new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port) } } class Port_Forwarding private[SSH]( ssh: SSH.Session, ssh_close: Boolean, val local_host: String, val local_port: Int, val remote_host: String, val remote_port: Int) extends AutoCloseable { override def toString: String = local_host + ":" + local_port + ":" + remote_host + ":" + remote_port def close() { ssh.session.delPortForwardingL(local_host, local_port) if (ssh_close) ssh.close() } } /* Sftp channel */ type Attrs = SftpATTRS sealed case class Dir_Entry(name: String, is_dir: Boolean) { def is_file: Boolean = !is_dir } /* exec channel */ private val exec_wait_delay = Time.seconds(0.3) class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable { override def toString: String = "exec " + session.toString def close() { channel.disconnect } val exit_status: Future[Int] = Future.thread("ssh_wait") { while (!channel.isClosed) Thread.sleep(exec_wait_delay.ms) channel.getExitStatus } val stdin: OutputStream = channel.getOutputStream val stdout: InputStream = channel.getInputStream val stderr: InputStream = channel.getErrStream // connect after preparing streams channel.connect(connect_timeout(session.options)) def result( progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true): Process_Result = { stdin.close def read_lines(stream: InputStream, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] val line_buffer = new ByteArrayOutputStream(100) def line_flush() { val line = Library.trim_line(line_buffer.toString(UTF8.charset_name)) progress(line) result += line line_buffer.reset } var c = 0 var finished = false while (!finished) { while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c) if (c == 10) line_flush() else if (channel.isClosed) { if (line_buffer.size > 0) line_flush() finished = true } else Thread.sleep(exec_wait_delay.ms) } result.toList } val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) } val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) } def terminate() { close out_lines.join err_lines.join exit_status.join } val rc = try { exit_status.join } catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } close if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() Process_Result(rc, out_lines.join, err_lines.join) } } /* session */ class Session private[SSH]( val options: Options, val session: JSch_Session, on_close: () => Unit) extends System with AutoCloseable { def update_options(new_options: Options): Session = new Session(new_options, session, on_close) def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@" def host: String = if (session.getHost == null) "" else session.getHost def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort override def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/" override def prefix: String = user_prefix + host + port_suffix + ":" override def toString: String = user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)") /* port forwarding */ def port_forwarding( remote_port: Int, remote_host: String = "localhost", local_port: Int = 0, local_host: String = "localhost", ssh_close: Boolean = false): Port_Forwarding = Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port) /* sftp channel */ val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp] sftp.connect(connect_timeout(options)) def close() { sftp.disconnect; session.disconnect; on_close() } val settings: Map[String, String] = { val home = sftp.getHome Map("HOME" -> home, "USER_HOME" -> home) } override def expand_path(path: Path): Path = path.expand_env(settings) def remote_path(path: Path): String = expand_path(path).implode override def bash_path(path: Path): String = Bash.string(remote_path(path)) def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path)) def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2)) def rm(path: Path): Unit = sftp.rm(remote_path(path)) def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path)) def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path)) private def test_entry(path: Path, as_dir: Boolean): Boolean = try { val is_dir = sftp.stat(remote_path(path)).isDir if (as_dir) is_dir else !is_dir } catch { case _: SftpException => false } override def is_dir(path: Path): Boolean = test_entry(path, true) override def is_file(path: Path): Boolean = test_entry(path, false) def is_link(path: Path): Boolean = try { sftp.lstat(remote_path(path)).isLink } catch { case _: SftpException => false } override def mkdirs(path: Path): Unit = if (!is_dir(path)) { execute( "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"") if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path))) } def read_dir(path: Path): List[Dir_Entry] = { if (!is_dir(path)) error("No such directory: " + path.toString) val dir_name = remote_path(path) val dir = sftp.ls(dir_name) (for { i <- (0 until dir.size).iterator a = dir.get(i).asInstanceOf[AnyRef] name = Untyped.get[String](a, "filename") attrs = Untyped.get[Attrs](a, "attrs") if name != "." && name != ".." } yield { Dir_Entry(name, if (attrs.isLink) { try { sftp.stat(dir_name + "/" + name).isDir } catch { case _: SftpException => false } } else attrs.isDir) - }).toList + }).toList.sortBy(_.name) } def find_files( start: Path, pred: Path => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false): List[Path] = { val result = new mutable.ListBuffer[Path] def check(path: Path) { if (pred(path)) result += path } def find(dir: Path) { if (include_dirs) check(dir) if (follow_links || !is_link(dir)) { for (entry <- read_dir(dir)) { val path = dir + Path.basic(entry.name) if (entry.is_file) check(path) else find(path) } } } if (is_file(start)) check(start) else find(start) result.toList } def open_input(path: Path): InputStream = sftp.get(remote_path(path)) def open_output(path: Path): OutputStream = sftp.put(remote_path(path)) def read_file(path: Path, local_path: Path): Unit = sftp.get(remote_path(path), File.platform_path(local_path)) def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) def read(path: Path): String = using(open_input(path))(File.read_stream(_)) def write_file(path: Path, local_path: Path): Unit = sftp.put(File.platform_path(local_path), remote_path(path)) def write_bytes(path: Path, bytes: Bytes): Unit = using(open_output(path))(bytes.write_stream(_)) def write(path: Path, text: String): Unit = using(open_output(path))(stream => Bytes(text).write_stream(stream)) /* exec channel */ def exec(command: String): Exec = { val channel = session.openChannel("exec").asInstanceOf[ChannelExec] channel.setCommand("export USER_HOME=\"$HOME\"\n" + command) new Exec(this, channel) } override def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true): Process_Result = exec(command).result(progress_stdout, progress_stderr, strict) /* tmp dirs */ def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) def rm_tree(remote_dir: String): Unit = execute("rm -r -f " + Bash.string(remote_dir)).check def tmp_dir(): String = execute("mktemp -d -t tmp.XXXXXXXXXX").check.out def with_tmp_dir[A](body: Path => A): A = { val remote_dir = tmp_dir() try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) } } } /* system operations */ trait System { def hg_url: String = "" def prefix: String = "" def expand_path(path: Path): Path = path.expand def bash_path(path: Path): String = File.bash_path(path) def is_dir(path: Path): Boolean = path.is_dir def is_file(path: Path): Boolean = path.is_file def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path) def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true): Process_Result = Isabelle_System.bash(command, progress_stdout = progress_stdout, progress_stderr = progress_stderr, strict = strict) } object Local extends System } diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,377 +1,385 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult} import java.nio.file.attribute.BasicFileAttributes import scala.collection.mutable object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ @volatile private var _settings: Option[Map[String, String]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty) { import scala.collection.JavaConversions._ val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") else "" if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) def set_cygwin_root() { if (Platform.is_windows) _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) } set_cygwin_root() def default(env: Map[String, String], entry: (String, String)): Map[String, String] = if (env.isDefinedAt(entry._1) || entry._2 == "") env else env + entry val env = { val temp_windows = { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" } val user_home = System.getProperty("user.home", "") val isabelle_app = System.getProperty("isabelle.app", "") default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") } val settings = { val dump = JFile.createTempFile("settings", null) dump.deleteOnExit try { val cmd1 = if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l", File.standard_path(isabelle_root1 + "\\bin\\isabelle")) else List(isabelle_root1 + "/bin/isabelle") val cmd = cmd1 ::: List("getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output) val entries = (for (entry <- File.read(dump).split("\u0000") if entry != "") yield { val i = entry.indexOf('=') if (i <= 0) entry -> "" else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } finally { dump.delete } } _settings = Some(settings) set_cygwin_root() } } /* getenv */ def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") def isabelle_id(): String = proper_string(getenv("ISABELLE_ID")) getOrElse Mercurial.repository(Path.explode("~~")).parent() /** file-system operations **/ /* directories */ def mkdirs(path: Path): Unit = if (!path.is_dir) { bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"") if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path))) } def copy_dir(dir1: Path, dir2: Path): Unit = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check /* tmp files */ private def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: Path): Unit = rm_tree(root.file) def rm_tree(root: JFile) { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit) { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) File.move(dir, old_dir) File.move(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close proc.getErrorStream.close proc.destroy Thread.interrupted } (output, rc) } def kill(signal: String, group_pid: String): (String, Int) = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), progress_limit: Option[Long] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout, progress_stderr, progress_limit, strict) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } - def gnutar(args: String, cwd: JFile = null, redirect: Boolean = false): Process_Result = + def gnutar( + args: String, + dir: Path = Path.current, + original_owner: Boolean = false, + redirect: Boolean = false): Process_Result = { - if (gnutar_check) bash("tar " + args, cwd = cwd, redirect = redirect) + val options = + (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + + (if (original_owner) "" else "--owner=root --group=staff ") + + if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* classes */ def init_classes[A](variable: String): List[A] = { for (name <- space_explode(':', Isabelle_System.getenv_strict(variable))) yield { def err(msg: String): Nothing = error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[A]].newInstance() } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } } /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC") } } } diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala +++ b/src/Pure/System/isabelle_tool.scala @@ -1,175 +1,176 @@ /* Title: Pure/System/isabelle_tool.scala Author: Makarius Author: Lars Hupel Isabelle system tools: external executables or internal Scala functions. */ package isabelle import java.net.URLClassLoader import scala.reflect.runtime.universe import scala.tools.reflect.{ToolBox,ToolBoxError} object Isabelle_Tool { /* Scala source tools */ abstract class Body extends Function[List[String], Unit] private def compile(path: Path): Body = { def err(msg: String): Nothing = cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path) val source = File.read(path) val class_loader = new URLClassLoader(Array(), getClass.getClassLoader) val tool_box = universe.runtimeMirror(class_loader).mkToolBox() try { val symbol = tool_box.parse(source) match { case tree: universe.ModuleDef => tool_box.define(tree) case _ => err("Source does not describe a module (Scala object)") } tool_box.compile(universe.Ident(symbol))() match { case body: Body => body case _ => err("Ill-typed source: Isabelle_Tool.Body expected") } } catch { case e: ToolBoxError => if (tool_box.frontEnd.hasErrors) { val infos = tool_box.frontEnd.infos.toList val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg) err(msgs.mkString("\n")) } else err(e.toString) } } /* external tools */ private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS")) private def is_external(dir: Path, file_name: String): Boolean = { val file = (dir + Path.explode(file_name)).file try { file.isFile && file.canRead && (file_name.endsWith(".scala") || file.canExecute) && !file_name.endsWith("~") && !file_name.endsWith(".orig") } catch { case _: SecurityException => false } } private def list_external(): List[(String, String)] = { val Description = """.*\bDESCRIPTION: *(.*)""".r for { dir <- dirs() if dir.is_dir file_name <- File.read_dir(dir) if is_external(dir, file_name) } yield { val source = File.read(dir + Path.explode(file_name)) val name = Library.perhaps_unsuffix(".scala", file_name) val description = split_lines(source).collectFirst({ case Description(s) => s }) getOrElse "" (name, description) } } private def find_external(name: String): Option[List[String] => Unit] = dirs.collectFirst({ case dir if is_external(dir, name + ".scala") => compile(dir + Path.explode(name + ".scala")) case dir if is_external(dir, name) => (args: List[String]) => { val tool = dir + Path.explode(name) val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) sys.exit(result.print_stdout.rc) } }) /* internal tools */ private lazy val internal_tools: List[Isabelle_Tool] = Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS") .flatMap(_.tools.toList) private def list_internal(): List[(String, String)] = for (tool <- internal_tools.toList) yield (tool.name, tool.description) private def find_internal(name: String): Option[List[String] => Unit] = internal_tools.collectFirst({ case tool if tool.name == name => args => Command_Line.tool0 { tool.body(args) } }) /* command line entry point */ def main(args: Array[String]) { Command_Line.tool0 { args.toList match { case Nil | List("-?") => val tool_descriptions = (list_external() ::: list_internal()).sortBy(_._1). map({ case (a, "") => a case (a, b) => a + " - " + b }) Getopts(""" Usage: isabelle TOOL [ARGS ...] Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage case tool_name :: tool_args => find_external(tool_name) orElse find_internal(tool_name) match { case Some(tool) => tool(tool_args) case None => error("Unknown Isabelle tool: " + quote(tool_name)) } } } } } sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit) class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) class Regular_Tools extends Isabelle_Scala_Tools( Build.isabelle_tool, Build_Docker.isabelle_tool, Doc.isabelle_tool, Dump.isabelle_tool, Export.isabelle_tool, Imports.isabelle_tool, ML_Process.isabelle_tool, Mkroot.isabelle_tool, Options.isabelle_tool, Present.isabelle_tool, Profiling_Report.isabelle_tool, Server.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Comments.isabelle_tool, Update_Header.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, isabelle.vscode.Grammar.isabelle_tool, isabelle.vscode.Server.isabelle_tool) class Admin_Tools extends Isabelle_Scala_Tools( Build_Cygwin.isabelle_tool, Build_Doc.isabelle_tool, Build_Fonts.isabelle_tool, Build_JDK.isabelle_tool, Build_PolyML.isabelle_tool1, Build_PolyML.isabelle_tool2, Build_Status.isabelle_tool, Check_Sources.isabelle_tool, + Components.isabelle_tool, isabelle.vscode.Build_VSCode.isabelle_tool) diff --git a/src/Pure/build-jars b/src/Pure/build-jars --- a/src/Pure/build-jars +++ b/src/Pure/build-jars @@ -1,316 +1,316 @@ #!/usr/bin/env bash # # Author: Makarius # # build-jars - build Isabelle/Scala # # Requires proper Isabelle settings environment. ## sources declare -a SOURCES=( Admin/afp.scala Admin/build_cygwin.scala Admin/build_doc.scala Admin/build_fonts.scala Admin/build_history.scala Admin/build_jdk.scala Admin/build_log.scala Admin/build_polyml.scala Admin/build_release.scala Admin/build_status.scala Admin/check_sources.scala Admin/ci_profile.scala + Admin/components.scala Admin/isabelle_cronjob.scala Admin/isabelle_devel.scala Admin/jenkins.scala Admin/other_isabelle.scala Concurrent/consumer_thread.scala Concurrent/counter.scala Concurrent/event_timer.scala Concurrent/future.scala Concurrent/mailbox.scala Concurrent/par_list.scala Concurrent/standard_thread.scala Concurrent/synchronized.scala GUI/color_value.scala GUI/gui.scala GUI/gui_thread.scala GUI/popup.scala GUI/wrap_panel.scala General/antiquote.scala General/bytes.scala General/cache.scala General/codepoint.scala General/comment.scala General/completion.scala General/csv.scala General/date.scala General/exn.scala General/file.scala General/file_watcher.scala General/graph.scala General/graph_display.scala General/graphics_file.scala General/http.scala General/json.scala General/linear_set.scala General/logger.scala General/long_name.scala General/mercurial.scala General/multi_map.scala General/output.scala General/path.scala General/position.scala General/pretty.scala General/properties.scala General/scan.scala General/sha1.scala General/sql.scala General/ssh.scala General/symbol.scala General/time.scala General/timing.scala General/untyped.scala General/url.scala General/utf8.scala General/value.scala General/word.scala General/xz.scala Isar/document_structure.scala Isar/keyword.scala Isar/line_structure.scala Isar/outer_syntax.scala Isar/parse.scala Isar/token.scala ML/ml_console.scala ML/ml_lex.scala ML/ml_process.scala ML/ml_statistics.scala ML/ml_syntax.scala PIDE/command.scala PIDE/command_span.scala PIDE/document.scala PIDE/document_id.scala PIDE/document_status.scala PIDE/editor.scala PIDE/headless.scala PIDE/line.scala PIDE/markup.scala PIDE/markup_tree.scala PIDE/protocol.scala PIDE/protocol_handlers.scala PIDE/protocol_message.scala PIDE/prover.scala PIDE/query_operation.scala PIDE/rendering.scala PIDE/resources.scala PIDE/session.scala PIDE/text.scala PIDE/xml.scala PIDE/yxml.scala ROOT.scala System/bash.scala System/command_line.scala - System/components.scala System/cygwin.scala System/distribution.scala System/getopts.scala System/invoke_scala.scala System/isabelle_charset.scala System/isabelle_fonts.scala System/isabelle_process.scala System/isabelle_system.scala System/isabelle_tool.scala System/numa.scala System/options.scala System/platform.scala System/posix_interrupt.scala System/process_result.scala System/progress.scala System/system_channel.scala System/tty_loop.scala Thy/bibtex.scala Thy/export.scala Thy/export_theory.scala Thy/file_format.scala Thy/html.scala Thy/latex.scala Thy/present.scala Thy/sessions.scala Thy/thy_element.scala Thy/thy_header.scala Thy/thy_syntax.scala Tools/build.scala Tools/build_docker.scala Tools/check_keywords.scala Tools/debugger.scala Tools/doc.scala Tools/dump.scala Tools/fontforge.scala Tools/imports.scala Tools/main.scala Tools/mkroot.scala Tools/print_operation.scala Tools/profiling_report.scala Tools/server.scala Tools/server_commands.scala Tools/simplifier_trace.scala Tools/spell_checker.scala Tools/task_statistics.scala Tools/update_cartouches.scala Tools/update_comments.scala Tools/update_header.scala Tools/update_then.scala Tools/update_theorems.scala library.scala pure_thy.scala term.scala term_xml.scala ../Tools/Graphview/graph_file.scala ../Tools/Graphview/graph_panel.scala ../Tools/Graphview/graphview.scala ../Tools/Graphview/layout.scala ../Tools/Graphview/main_panel.scala ../Tools/Graphview/metrics.scala ../Tools/Graphview/model.scala ../Tools/Graphview/mutator.scala ../Tools/Graphview/mutator_dialog.scala ../Tools/Graphview/mutator_event.scala ../Tools/Graphview/popups.scala ../Tools/Graphview/shapes.scala ../Tools/Graphview/tree_panel.scala ../Tools/VSCode/src/build_vscode.scala ../Tools/VSCode/src/channel.scala ../Tools/VSCode/src/document_model.scala ../Tools/VSCode/src/dynamic_output.scala ../Tools/VSCode/src/grammar.scala ../Tools/VSCode/src/preview_panel.scala ../Tools/VSCode/src/protocol.scala ../Tools/VSCode/src/server.scala ../Tools/VSCode/src/state_panel.scala ../Tools/VSCode/src/vscode_javascript.scala ../Tools/VSCode/src/vscode_rendering.scala ../Tools/VSCode/src/vscode_resources.scala ../Tools/VSCode/src/vscode_spell_checker.scala ) ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS]" echo echo " Options are:" echo " -f fresh build" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } [ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment" ## process command line # options FRESH="" while getopts "f" OPT do case "$OPT" in f) FRESH=true ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -ne 0 ] && usage ## build TARGET_DIR="$ISABELLE_HOME/lib/classes" TARGET="$TARGET_DIR/Pure.jar" declare -a UPDATED=() if [ -n "$FRESH" ]; then OUTDATED=true else OUTDATED=false if [ ! -e "$TARGET" ]; then OUTDATED=true else for DEP in "${SOURCES[@]}" do [ ! -e "$DEP" ] && fail "Missing file: $DEP" [ "$DEP" -nt "$TARGET" ] && { OUTDATED=true UPDATED["${#UPDATED[@]}"]="$DEP" } done fi fi if [ "$OUTDATED" = true ] then echo "### Building Isabelle/Scala ..." [ "${#UPDATED[@]}" -gt 0 ] && { echo "Changed files:" for FILE in "${UPDATED[@]}" do echo " $FILE" done } rm -f "$TARGET" rm -rf classes && mkdir classes SCALAC_OPTIONS="$ISABELLE_SCALAC_OPTIONS -d classes" ( classpath classes export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" isabelle_scala scalac $SCALAC_OPTIONS "${SOURCES[@]}" || \ fail "Failed to compile sources" ) || exit "$?" mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR" pushd classes >/dev/null CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider" mkdir -p "$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE" cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" isabelle/. cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" isabelle/. isabelle_jdk jar cfe "$(platform_path "$TARGET")" isabelle.Main META-INF isabelle || \ fail "Failed to produce $TARGET" popd >/dev/null rm -rf classes fi