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/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
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
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
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
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
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
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
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
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/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,810 +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 + "_linux.tar.gz", None)
- case Platform.Family.macos =>
- Bundle_Info(platform, "Mac OS X", dist_name + ".dmg", Some(dist_name + "_macos.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, 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, "-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)
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")
// 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.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="))
// MacOS application bundle
File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
- val dmg_dir = tmp_dir + Path.explode("macos_app/dmg")
val isabelle_app = Path.explode(isabelle_name + ".app")
- val app_dir = dmg_dir + isabelle_app
- File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir)
+ 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)
- // application archive: dmg or .tar.gz
-
- val isabelle_dmg = Path.explode(isabelle_name + ".dmg")
- (release.dist_dir + isabelle_dmg).file.delete
-
- remote_mac match {
- case SSH.Target(user, host) =>
- progress.echo("Packaging " + isabelle_dmg + " (via host " + quote(host) + ") ...")
- using(SSH.open_session(options, host = host, user = user))(ssh =>
- {
- val dmg_archive = Path.explode("dmg.tar")
- execute_tar(dmg_dir, "-cf " + File.bash_path(tmp_dir + dmg_archive) + " .")
+ // application archive
- ssh.with_tmp_dir(remote_dir =>
- {
- val cd = "cd " + ssh.bash_path(remote_dir) + "; "
- ssh.write_file(remote_dir + dmg_archive, tmp_dir + dmg_archive)
- ssh.execute(
- cd + "mkdir dmg && tar -C dmg -xf " + ssh.bash_path(dmg_archive)).check
- ssh.execute(
- cd + "hdiutil create -srcfolder dmg -volname Isabelle " +
- ssh.bash_path(isabelle_dmg)).check
- ssh.read_file(remote_dir + isabelle_dmg, release.dist_dir + isabelle_dmg)
- })
- })
- case _ =>
- val archive_name = isabelle_name + "_macos.tar.gz"
- progress.echo("Packaging " + archive_name + " ...")
- execute_tar(dmg_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
- File.bash_path(isabelle_app))
- }
+ 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)
}
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 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, "-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/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))
}
}