diff --git a/Admin/components/components.sha1 b/Admin/components/components.sha1
--- a/Admin/components/components.sha1
+++ b/Admin/components/components.sha1
@@ -1,408 +1,409 @@
59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz
23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz
eccff31931fb128c1dd522cfc85495c9b66e67af Haskabelle-2015.tar.gz
ed740867925dcf58692c8d3e350c28e3b4d4a60f Isabelle_app-20210126.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
5c5b7c18cc1dc2a4d22b997dac196da09eaca868 bash_process-1.2.3-1.tar.gz
48b01bd9436e243ffcb7297f08b498d0c0875ed9 bash_process-1.2.3.tar.gz
11815d5f3af0de9022e903ed8702c136591f06fe bash_process-1.2.4-1.tar.gz
729486311833e4eff0fbf2d8041dddad520ca88c bash_process-1.2.4-2.tar.gz
7ae9ec8aab2d8a811842d9dc67d8bf6c179e11ee bash_process-1.2.4.tar.gz
9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz
a65ce644b6094d41e9f991ef851cf05eff5dd0a9 bib2xhtml-20171221.tar.gz
4085dd6060a32d7e0d2e3f874c463a9964fd409b bib2xhtml-20190409.tar.gz
f92cff635dfba5d4d77f469307369226c868542c cakeml-2.0.tar.gz
e7ffe4238b61a3c1ee87aca4421e7a612e09b836 ci-extras-1.tar.gz
e880f31f59bd403fb72fcd3b5afb413c3831a21c csdp-6.1-1.tar.gz
2659100ba8e28e7cb0ecb554178ee5315d4a87f5 csdp-6.1.1.tar.gz
a2bd94f4f9281dc70dfda66cf28016c2ffef7ed7 csdp-6.1.tar.gz
ec17080269737e4a97b4424a379924c09b338ca2 csdp-6.2.0.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
ffb0d4739c10eb098eb092baef13eccf94a79bad cvc4-1.5-5.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
e99560d0b7cb9bafde2b0ec1a3a95af315918a25 cvc4-1.8.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
2aa049170e8088de59bd70eed8220f552093932d cygwin-20190320.tar.gz
fb898e263fcf6f847d97f564fe49ea0760bb453f cygwin-20190322.tar.gz
cd01fac0ab4fdb50a2bbb6416da3f15a4d540da1 cygwin-20190524.tar.gz
caa616fbab14c1fce790a87db5c4758c1322cf28 cygwin-20200116.tar.gz
f053a9ab01f0be9cb456560f7eff66a8e7ba2fd2 cygwin-20200323.tar.gz
0107343cd2562618629f73b2581168f0045c3234 cygwin-20201002.tar.gz
a3d481401b633c0ee6abf1da07d75da94076574c cygwin-20201130.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
fac44556dd16f666a2c186be30aa6d8c67228bb9 e-2.0-3.tar.gz
5d36fb62912cfcff7f3b99a6266c578aafc288b7 e-2.0-4.tar.gz
3223c51c0b16fe00ced4ae903041fff858e61742 e-2.0-5.tar.gz
6b962a6b4539b7ca4199977973c61a8c98a492e8 e-2.0.tar.gz
66449a7b68b7d85a7189e10735a81069356123b6 e-2.5-1.tar.gz
813b66ca151d7a39b5cacb39ab52acabc2a54845 e-2.5.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
7a4b46752aa60c1ee6c53a2c128dedc8255a4568 flatlaf-0.46-1.tar.gz
ed5cbc216389b655dac21a19e770a02a96867b85 flatlaf-0.46.tar.gz
d37b38b9a27a6541c644e22eeebe9a339282173d flatlaf-1.0-rc1.tar.gz
dac46ce81cee10fb36a9d39b414dec7b7b671545 flatlaf-1.0-rc2.tar.gz
d94e6da7299004890c04a7b395a3f2d381a3281e flatlaf-1.0-rc3.tar.gz
7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz
f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.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
928b5320073d04d93bcc5bc4347b6d01632b9d45 isabelle_fonts-20190210.tar.gz
dfcdf9a757b9dc36cee87f82533b43c58ba84abe isabelle_fonts-20190309.tar.gz
95e3acf038df7fdeeacd8b4769930e6f57bf3692 isabelle_fonts-20190406.tar.gz
dabcf5085d67c99159007007ff0e9bf775e423d1 isabelle_fonts-20190409.tar.gz
76827987c70051719e117138858930d42041f57d isabelle_fonts-20190717.tar.gz
abc8aea3ae471f9313917008ac90e5c1c99e17da isabelle_fonts-20210317.tar.gz
3ff9195aab574fc75ca3b77af0adb33f9b6d7b74 isabelle_fonts-20210318.tar.gz
b166b4bd583b6442a5d75eab06f7adbb66919d6d isabelle_fonts-20210319.tar.gz
9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz
1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
06ac8993b5bebd02c70f1bd18ce13075f01115f3 jdk-11.0.3+7.tar.gz
e7e3cc9b0550c1e5d71197ad8c30f92b622d7183 jdk-11.0.4+11.tar.gz
49007a84a2643a204ce4406770dfd574b97880d9 jdk-11.0.5+10.tar.gz
3c250e98eb82f98afc6744ddc9170d293f0677e1 jdk-11.0.6+10.tar.gz
76cf7a141e15db30bd975089c65c833b58092aa7 jdk-11.0.9+11.tar.gz
71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz
72455a2fdb6cced9cd563f4d5d6134f7a6c34913 jdk-15.0.1+9.tar.gz
e8ae300e61b0b121018456d50010b555bc96ce10 jdk-15.0.2+7.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
536a38ed527115b4bf2545a2137ec57b6ffad718 jedit_build-20190120.tar.gz
58b9f03e5ec0b85f8123c31f5d8092dae5803773 jedit_build-20190130.tar.gz
ec0aded5f2655e2de8bc4427106729e797584f2f jedit_build-20190224.tar.gz
1e53598a02ec8d8736b15f480cbe2c84767a7827 jedit_build-20190508.tar.gz
b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz
1c753beb93e92e95e99e8ead23a68346bd1af44a jedit_build-20200610.tar.gz
533b1ee6459f59bcbe4f09e214ad2cb990fb6952 jedit_build-20200908.tar.gz
f9966b5ed26740bb5b8bddbfe947fcefaea43d4d jedit_build-20201223.tar.gz
0bdbd36eda5992396e9c6b66aa24259d4dd7559c jedit_build-20210201.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
d84b7d8ef273afec55284327fca7dd20f5ecb77a jfreechart-1.5.1.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
0634a946b216f7f07f1a0f7e28cf345daa28828f kodkodi-1.5.3.tar.gz
52e95b3493d71902f9df89d0bb59d0046a5f0c63 kodkodi-1.5.4-1.tar.gz
267189c637de26cf304d699cfa95389da002b250 kodkodi-1.5.4.tar.gz
3ecdade953bb455ed2907952be287d7e5cf6533b kodkodi-1.5.5.tar.gz
8aa939f5127290eb9a99952d375be9ffbf90c43b kodkodi-1.5.6-1.tar.gz
6b12bf3f40b16fae8ff22aa39171fa018d107cb3 kodkodi-1.5.6.tar.gz
377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
759848095e2ad506083d92b5646947e3c32f27a0 linux_app-20191223.tar.gz
1a449ce69ac874e21804595d16aaaf5a0d0d0c10 linux_app-20200110.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
0fbc826e4fcb95bb9e1814642f7fce788e7fe1c3 naproche-20210122-1.tar.gz
eda10c62da927a842c0a8881f726eac85e1cb4f7 naproche-20210122.tar.gz
edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz
d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300 naproche-20210129.tar.gz
810ee0f35adada9bf970c33fd80b986ab2255bf3 naproche-20210201.tar.gz
4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz
77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz
9c02ecf93863c3289002c5e5ac45a83e2505984c naproche-755224402e36.tar.gz
e1b34e8f54e7e5844873612635444fed434718a1 naproche-7d0947a91dd5.tar.gz
26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz
e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz
fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz
eb499a18e7040ca0fe1ca824c9dcb2087c47c9ba opam-2.0.3-1.tar.gz
002f74c9e65e650de2638bf54d7b012b8de76c28 opam-2.0.3.tar.gz
ddb3b438430d9565adbf5e3d913bd52af8337511 opam-2.0.6.tar.gz
fc66802c169f44511d3be30435eb89a11e635742 opam-2.0.7.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
51e024225b460900da5279f0b91b217085f98cf9 polyml-5.8-20190220.tar.gz
20a83fa58d497b533150defe39bcd4540529b25f polyml-5.8-20190306.tar.gz
9f0e9cd10df4c3383b063eb076e8b698ca50c3d0 polyml-5.8.1-20191101.tar.gz
f46deb909d645ac8c140968e4d32b5763beb9add polyml-5.8.1-20191113.tar.gz
36a40a981b57daae0463d14940a8edf6fa1af179 polyml-5.8.1-20191114.tar.gz
525b05536b08c11a1eae943fe6818a8622326084 polyml-5.8.1-20191124.tar.gz
9043828803483ca14df64488dff014ad050a6d34 polyml-5.8.1-20200228.tar.gz
1186607e2c43b77db86731f12fbedb531ca50a21 polyml-5.8.1-20200708.tar.gz
22ae16bf7850e73b903d2ca8eb506da05b441cf3 polyml-5.8.1.tar.gz
+cb8e85387315f62dcfc6b21ec378186e58068f76 polyml-5.8.2.tar.gz
d1fd6eced69dc1df7226432fcb824568e0994ff2 polyml-5.8.tar.gz
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
8e83fb5088cf265902b8da753a8eac5fe3f6a14b polyml-test-159dc81efc3b.tar.gz
a0064c157a59e2706e18512a49a6dca914fa17fc polyml-test-1b2dcf8f5202.tar.gz
4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz
853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
85bfda83d138e936fdafd68ed3627b1058e5c2c3 polyml-test-7e49fce62e3d.tar.gz
c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz
7df4857d73dbc9edda25a6ad329e47639e70fadf polyml-test-8fda4fd22441.tar.gz
2b7c02b67feb2f44dda6938a7244f4257e7c580c polyml-test-905dae2ebfda.tar.gz
3dfdc58e5d9b28f038a725e05c9c2f2ce0bb2632 polyml-test-a3cfdf648da-1.tar.gz
e2f075b0cc709f4f7f6492b725362f9010b2c6d1 polyml-test-a3cfdf648da-2.tar.gz
33568f69ce813b7405386ddbefa14ad0342bb8f0 polyml-test-a3cfdf648da.tar.gz
4bedaac4f1fb9a9199aa63695735063c47059003 polyml-test-a444f281ccec.tar.gz
f3031692edcc5d8028a42861e4e40779f0f9d3e1 polyml-test-b68438d33c69.tar.gz
cb2318cff6ea9293cd16a4435a4fe28ad9dbe0b8 polyml-test-cf46747fee61.tar.gz
67ffed2f98864721bdb1e87f0ef250e4c69e6160 polyml-test-d68c6736402e.tar.gz
b4ceeaac47f3baae41c2491a8368b03217946166 polyml-test-e7a662f8f9c4.tar.gz
609c7d09d3ed01156ff91261e801e2403ff93729 polyml-test-e8d82343b692.tar.gz
b6d87466e9b44e8ef4a2fac74c96b139080a506a polyml-test-f54aa41240d0.tar.gz
d365f3fc11c2427cafc62b3c79951880a1476ebb polyml-test-f86ae3dc1686.tar.gz
a619177143fea42a464f49bb864665407c07a16c polyml-test-fb4f42af00fa.tar.gz
53123dc011b2d4b4e8fe307f3c9fa355718ad01a postgresql-42.1.1.tar.gz
3a5d31377ec07a5069957f5477a4848cfc89a594 postgresql-42.1.4.tar.gz
7d6ef4320d5163ceb052eb83c1cb3968f099a422 postgresql-42.2.18.tar.gz
e7cd5c7955e9eb5ce8cd07feb97230b23d2eec40 postgresql-42.2.2.tar.gz
231b33c9c3c27d47e3ba01b399103d70509e0731 postgresql-42.2.5.tar.gz
6335fbc0658e447b5b9bc48c9ad36e33a05bb72b postgresql-42.2.9.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
059cbdc58d36e3ac1fffcccd9139ecd34f271882 scala-2.12.10.tar.gz
82056106aa6fd37c159ea76d16096c20a749cccd scala-2.12.11.tar.gz
fe7ff585acffaad7f0dd4a1d079134d15c26ed0d scala-2.12.12.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
201c05ae9cc382ee6c08af49430e426f6bbe0d5a scala-2.12.8.tar.gz
a0622fe75c3482ba7dc3ce74d58583b648a1ff0d scala-2.13.4-1.tar.gz
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.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
edaa1268d82203067657aabcf0371ce7d4b579b9 spass-3.8ds-2.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
4d17611857fa3a93944c1f159c0fd2a161967aaf sqlite-jdbc-3.27.2.1.tar.gz
806be457eb79408fcc5a72aeca3f64b2d89a6b63 sqlite-jdbc-3.30.1.tar.gz
cba2b194114216b226d75d49a70d1bd12b141ac8 sqlite-jdbc-3.32.3.2.tar.gz
29306acd6ce9f4c87032b2c271c6df035fe7d4d3 sqlite-jdbc-3.34.0.tar.gz
8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz
2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz
a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz
fdc415284e031ee3eb2f65828cbc6945736fe995 stack-1.9.1.tar.gz
6e19948ff4a821e2052fc9b3ddd9ae343f4fcdbb stack-1.9.3.tar.gz
f969443705aa8619e93af5b34ea98d15cd7efaf1 stack-2.1.3.tar.gz
ebd0221d038966aa8bde075f1b0189ff867b02ca stack-2.5.1.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
a45eca5c1277f42f87bb8dc12a3074ccf5488221 sumatra_pdf-3.1.2-1.tar.gz
3b3239b2e6f8062b90d819f3703e30a50f4fa1e7 sumatra_pdf-3.1.2-2.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
52ba18a6c96b53c5ae9b179d5a805a0c08f1da6d verit-2020.10-rmx-1.tar.gz
b6706e74e20e14038e9b38f0acdb5639a134246a verit-2020.10-rmx.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
4c366ab255d2e9343fb635d44d4d55ddd24c76d0 z3-4.4.0pre-3.tar.gz
517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz
aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz
9dfeb39c87393af7b6a34118507637aa53aca05e zipperposition-2.0-1.tar.gz
b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz
diff --git a/Admin/components/main b/Admin/components/main
--- a/Admin/components/main
+++ b/Admin/components/main
@@ -1,29 +1,29 @@
#main components for everyday use, without big impact on overall build time
gnu-utils-20210414
bash_process-1.2.4-2
bib2xhtml-20190409
csdp-6.1.1
cvc4-1.8
e-2.5-1
flatlaf-1.0
isabelle_fonts-20210322
jdk-15.0.2+7
jedit_build-20210201
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6-1
nunchaku-0.5
opam-2.0.7
-polyml-test-f86ae3dc1686
+polyml-5.8.2
postgresql-42.2.18
scala-2.13.5
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.34.0
ssh-java-20190323
stack-2.5.1
vampire-4.2.2
verit-2020.10-rmx-1
xz-java-1.8
z3-4.4.0pre-3
zipperposition-2.0-1
diff --git a/Admin/etc/options b/Admin/etc/options
--- a/Admin/etc/options
+++ b/Admin/etc/options
@@ -1,22 +1,25 @@
(* :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"
+option build_host_linux_arm : string = ""
+ -- "SSH user@host for remote build of heaps"
+
option build_host_linux : string = ""
-- "SSH user@host for remote build of heaps"
option build_host_macos : string = ""
-- "SSH user@host for remote build of heaps"
option build_host_windows : string = ""
-- "SSH user@host for remote build of heaps"
diff --git a/Admin/polyml/README b/Admin/polyml/README
--- a/Admin/polyml/README
+++ b/Admin/polyml/README
@@ -1,51 +1,52 @@
Poly/ML for Isabelle
====================
-This compilation of Poly/ML (http://www.polyml.org) is based on the
-repository version
-https://github.com/polyml/polyml/commit/f86ae3dc1686
+This compilation of Poly/ML (https://www.polyml.org) is based on the
+source distribution from
+https://github.com/polyml/polyml/commits/fixes-5.8.2 up to commit
+e6a463e1614f.
The Isabelle repository provides an administrative tool "isabelle
build_polyml", which can be used in the polyml component directory as
follows.
* Linux:
$ isabelle build_polyml -m32 -s sha1 src
$ isabelle build_polyml -m64 -s sha1 src
* macOS:
$ isabelle build_polyml -m32 -s sha1 src
$ isabelle build_polyml -m64 -s sha1 src
* Windows (Cygwin shell)
$ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
$ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
Building libgmp on macOS
========================
The build_polyml invocations above implicitly use the GNU Multiple Precision
Arithmetic Library (libgmp), but that is not available on macOS by default.
Appending "--without-gmp" to the command-line omits this library. Building
libgmp properly from sources works as follows (library headers and binaries
will be placed in /usr/local).
* Download:
$ curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz | xz -dc | tar xf -
$ cd gmp-6.1.2
* build:
$ make distclean
$ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
$ make && make check
$ sudo make install
Makarius
- 19-Nov-2020
+ 07-May-2021
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,935 +1,937 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release
{
/** release context **/
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
private def execute_tar(dir: Path, args: String, strip: Int = 0): Unit =
Isabelle_System.gnutar(args, dir = dir, strip = strip).check
object Release_Context
{
def apply(
target_dir: Path,
release_name: String = "",
components_base: Path = Components.default_components_base,
progress: Progress = new Progress): Release_Context =
{
val date = Date.now()
val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
new Release_Context(release_name, dist_name, dist_dir, components_base, progress)
}
}
class Release_Context private[Build_Release](
val release_name: String,
val dist_name: String,
val dist_dir: Path,
val components_base: Path,
val progress: Progress)
{
override def toString: String = dist_name
val isabelle: Path = Path.explode(dist_name)
val isabelle_dir: Path = dist_dir + isabelle
val isabelle_archive: Path = dist_dir + isabelle.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 + isabelle,
isabelle_identifier = dist_name + "-build",
progress = progress)
def make_announce(id: String): Unit =
{
if (release_name.isEmpty) {
File.write(isabelle_dir + Path.explode("ANNOUNCE"),
"""
IMPORTANT NOTE
==============
This is a snapshot of Isabelle/""" + id + """ from the repository.
""")
}
}
def make_contrib(): Unit =
{
Isabelle_System.make_directory(Components.contrib(isabelle_dir))
File.write(Components.contrib(isabelle_dir, name = "README"),
"""This directory contains add-on components that contribute to the main
Isabelle distribution. Separate licensing conditions apply, see each
directory individually.
""")
}
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
case Platform.Family.linux_arm =>
Bundle_Info(platform, "Linux (ARM)", dist_name + "_linux_arm.tar.gz")
case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String)
{
def path: Path = Path.explode(name)
}
/** release archive **/
val ISABELLE: Path = Path.basic("Isabelle")
val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID")
val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
object Release_Archive
{
def make(bytes: Bytes, rename: String = ""): Release_Archive =
{
Isabelle_System.with_tmp_dir("tmp")(dir =>
Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
{
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
Bytes.write(archive_path, bytes)
execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
val id = File.read(isabelle_dir + ISABELLE_ID)
val tags = File.read(isabelle_dir + ISABELLE_TAGS)
val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER)
val (bytes1, identifier1) =
if (rename.isEmpty || rename == identifier) (bytes, identifier)
else {
File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename)
Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename))
execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename))
(Bytes.read(archive_path), rename)
}
new Release_Archive(bytes1, id, tags, identifier1)
})
)
}
def read(path: Path, rename: String = ""): Release_Archive =
make(Bytes.read(path), rename = rename)
def get(url: String, rename: String = "", progress: Progress = new Progress): Release_Archive =
{
val bytes =
if (Path.is_wellformed(url)) Bytes.read(Path.explode(url))
else Isabelle_System.download(url, progress = progress).bytes
make(bytes, rename = rename)
}
}
case class Release_Archive private[Build_Release](
bytes: Bytes, id: String, tags: String, identifier: String)
{
override def toString: String = identifier
}
/** generated content **/
/* 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): Unit =
{
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
Platform.Family.list.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
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]): Unit =
{
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))
}
/** build release **/
/* build heaps */
private def build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path): Unit =
{
val server_option = "build_host_" + platform.toString
val ssh =
options.string(server_option) match {
case "" =>
if (Platform.family == platform) SSH.Local
else error("Undefined option " + server_option + ": cannot build heaps")
case SSH.Target(user, host) =>
SSH.open_session(options, host = host, user = user)
case s => error("Malformed option " + server_option + ": " + quote(s))
}
try {
Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
{
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
ssh.with_tmp_dir(remote_dir =>
{
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val remote_commands =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
"bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && "), settings = false).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
})
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
})
}
finally { ssh.close() }
}
/* Isabelle application */
def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit =
{
val title = "# Java runtime options"
File.write(path, (title :: options).map(_ + line_ending).mkString)
}
def make_isabelle_app(
platform: Platform.Family.Value,
isabelle_target: Path,
isabelle_name: String,
jdk_component: String,
classpath: List[Path],
dock_icon: Boolean = false): Unit =
{
val script = """#!/usr/bin/env bash
#
# Author: Makarius
#
# Main Isabelle application script.
# minimal Isabelle environment
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
unset "JAVA_TOOL_OPTIONS"
#paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
unset XMODIFIERS
COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """"
source "$COMPONENT/etc/settings"
# main
declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options"))
"$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup"
exec "$ISABELLE_JDK_HOME/bin/java" \
"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
-classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
""" + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \
""" else "") + """isabelle.Main "$@"
"""
val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(script_path, script)
File.set_executable(script_path, true)
val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
Isabelle_System.move_file(
component_dir + Path.explode(Platform.Family.standard(platform)) + Path.explode("Isabelle"),
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(component_dir)
}
def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit =
{
File.write(path, """
CFBundleDevelopmentRegion
English
CFBundleIconFile
isabelle.icns
CFBundleIdentifier
de.tum.in.isabelle
CFBundleDisplayName
""" + isabelle_name + """
CFBundleInfoDictionaryVersion
6.0
CFBundleName
""" + isabelle_name + """
CFBundlePackageType
APPL
CFBundleShortVersionString
""" + isabelle_name + """
CFBundleSignature
????
CFBundleVersion
""" + isabelle_rev + """
NSHumanReadableCopyright
LSMinimumSystemVersion
10.11
LSApplicationCategoryType
public.app-category.developer-tools
NSHighResolutionCapable
true
NSSupportsAutomaticGraphicsSwitching
true
CFBundleDocumentTypes
CFBundleTypeExtensions
thy
CFBundleTypeIconFile
theory.icns
CFBundleTypeName
Isabelle theory file
CFBundleTypeRole
Editor
LSTypeIsPackage
""")
}
/* main */
def use_release_archive(
context: Release_Context,
archive: Release_Archive,
id: String = ""): Unit =
{
if (id.nonEmpty && id != archive.id) {
error("Mismatch of release identification " + id + " vs. archive " + archive.id)
}
if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) {
Bytes.write(context.isabelle_archive, archive.bytes)
}
}
def build_release_archive(
context: Release_Context,
version: String,
parallel_jobs: Int = 1): Unit =
{
val progress = context.progress
val hg = Mercurial.repository(Path.ISABELLE_HOME)
val id =
try { hg.id(version) }
catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
if (context.isabelle_archive.is_file) {
progress.echo_warning("Found existing release archive: " + context.isabelle_archive)
use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id)
}
else {
progress.echo_warning("Preparing release " + context.dist_name + " ...")
Isabelle_System.new_directory(context.dist_dir)
hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files")
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(context.isabelle_dir + Path.explode(name)).file.delete
}
File.write(context.isabelle_dir + ISABELLE_ID, id)
File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id))
File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name)
context.make_announce(id)
context.make_contrib()
execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(context.isabelle_dir)
/* build tools and documentation */
val other_isabelle = context.other_isabelle(context.dist_dir)
other_isabelle.init_settings(
other_isabelle.init_components(
components_base = context.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(msg) => cat_error("Failed to build tools:", msg) }
try {
other_isabelle.bash(
"bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
other_isabelle.make_news()
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 release archive " + context.isabelle_archive + " ...")
execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""")
execute(context.dist_dir,
"""find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
execute_tar(context.dist_dir, "-czf " +
File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
}
}
+ def default_platform_families: List[Platform.Family.Value] = Platform.Family.list0
+
def build_release(
options: Options,
context: Release_Context,
afp_rev: String = "",
- platform_families: List[Platform.Family.Value] = Platform.Family.list,
+ platform_families: List[Platform.Family.Value] = default_platform_families,
more_components: List[Path] = Nil,
website: Option[Path] = None,
build_sessions: List[String] = Nil,
build_library: Boolean = false,
parallel_jobs: Int = 1): Unit =
{
val progress = context.progress
/* release directory */
val archive = Release_Archive.read(context.isabelle_archive)
for (path <- List(context.isabelle, ISABELLE)) {
Isabelle_System.rm_tree(context.dist_dir + path)
}
Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
{
Bytes.write(archive_path, archive.bytes)
val extract =
List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
map(name => context.dist_name + "/" + name)
execute_tar(context.dist_dir,
"-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
})
Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE)
/* make application bundles */
val bundle_infos = platform_families.map(context.bundle_info)
for (bundle_info <- bundle_infos) {
val isabelle_name = context.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(context.isabelle_archive))
val other_isabelle = context.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(context.components_base, bundled_components,
target_dir = Some(contrib_dir),
copy_dir = Some(context.dist_dir + Path.explode("contrib")),
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: List[String] =
(for {
variable <-
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_OPTIONS")
opt <- Word.explode(other_isabelle.getenv(variable))
}
yield {
val s = "-Dapple.awt.application.name="
if (opt.startsWith(s)) s + isabelle_name else 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_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
progress.echo("Building heaps " + commas_quote(build_sessions) + " ...")
build_heaps(options, platform, build_sessions, isabelle_target)
}
// application bundling
platform match {
case Platform.Family.linux_arm | Platform.Family.linux =>
File.change(isabelle_target + jedit_options,
_.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
File.change(isabelle_target + jedit_props,
_.replaceAll("console.fontsize=.*", "console.fontsize=18")
.replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
.replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
.replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
.replaceAll("view.fontsize=.*", "view.fontsize=24")
.replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
make_isabelle_options(
isabelle_target + Path.explode("Isabelle.options"), java_options)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath)
progress.echo("Packaging " + bundle_info.name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
File.change(isabelle_target + jedit_props,
_.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// macOS application bundle
val app_contents = isabelle_target + Path.explode("Contents")
for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
}
make_isabelle_plist(
app_contents + Path.explode("Info.plist"), isabelle_name, archive.id)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
classpath, dock_icon = true)
val isabelle_options = Path.explode("Isabelle.options")
make_isabelle_options(
isabelle_target + isabelle_options,
java_options ::: List("-Disabelle.app=true"))
// application archive
progress.echo("Packaging " + bundle_info.name + " ...")
val isabelle_app = Path.explode(isabelle_name + ".app")
Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
tmp_dir + isabelle_app)
execute_tar(tmp_dir,
"-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
File.change(isabelle_target + jedit_props,
_.replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
make_isabelle_options(
isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
java_options, line_ending = "\r\n")
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = bundle_info.path
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replace("{ISABELLE_NAME}", isabelle_name)
.replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
.replace("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replace("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replace("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replace("\\jdk\\", "\\" + jdk_component + "\\"))
execute(tmp_dir,
"\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
Isabelle_System.copy_file(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).replace("{MIRROR}", cygwin_mirror))
File.set_executable(isabelle_target + cygwin_bat, true)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
Isabelle_System.copy_file(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 archive_name = isabelle_name + ".7z"
val exe_archive = tmp_dir + Path.explode(archive_name)
exe_archive.file.delete
progress.echo("Packaging " + archive_name + " ...")
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"))
.replace("{ISABELLE_NAME}", isabelle_name)
Bytes.write(context.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
File.set_executable(context.dist_dir + isabelle_exe, true)
}
})
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
if (context.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id),
HTML.text("Isabelle/" + archive.id))
val afp_link =
HTML.link(Isabelle_System.afp_repository.changeset(afp_rev),
HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
List(HTML.title(context.dist_name)),
List(
HTML.section(context.dist_name),
HTML.subsection("Downloads"),
HTML.itemize(
List(HTML.link(context.dist_name + ".tar.gz", HTML.text("Source archive"))) ::
website_platform_bundles.map({ case (bundle, bundle_info) =>
List(HTML.link(bundle, HTML.text(bundle_info.platform_description + " bundle"))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
Isabelle_System.copy_file(context.isabelle_archive, dir)
for ((bundle, _) <- website_platform_bundles) {
Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
}
}
/* HTML library */
if (build_library) {
if (context.isabelle_library_archive.is_file) {
progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val bundle =
context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = context.other_isabelle(tmp_dir)
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
" " + Bash.string(context.dist_name + "/browser_info"))
})
}
}
}
/** command line entry point **/
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var afp_rev = ""
var components_base: Path = Components.default_components_base
var target_dir = Path.current
var release_name = ""
var source_archive = ""
var website: Option[Path] = None
var build_sessions: List[String] = Nil
var more_components: List[Path] = Nil
var parallel_jobs = 1
var build_library = false
var options = Options.init()
- var platform_families = Platform.Family.list
+ 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: """ +
Components.default_components_base + """)
-D DIR target directory (default ".")
-R RELEASE explicit release name
-S ARCHIVE use existing source archive (file or URL)
-W WEBSITE produce minimal website in given directory
-b SESSIONS build platform-specific session images (separated by commas)
-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: """ + Platform.Family.list.mkString(",") + """)
+ -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """)
-r REV Mercurial changeset id (default: ARCHIVE or RELEASE or tip)
Build Isabelle release in base directory, using the local repository clone.
""",
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Path.explode(arg)),
"D:" -> (arg => target_dir = Path.explode(arg)),
"R:" -> (arg => release_name = arg),
"S:" -> (arg => source_archive = arg),
"W:" -> (arg => website = Some(Path.explode(arg))),
"b:" -> (arg => build_sessions = space_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)
if (more_args.nonEmpty) getopts.usage()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
val progress = new Console_Progress()
def make_context(name: String): Release_Context =
Release_Context(target_dir,
release_name = name,
components_base = components_base,
progress = progress)
val context =
if (source_archive.isEmpty) {
val context = make_context(release_name)
val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
build_release_archive(context, version, parallel_jobs = parallel_jobs)
context
}
else {
val archive =
Release_Archive.get(source_archive, rename = release_name, progress = progress)
val context = make_context(archive.identifier)
Isabelle_System.make_directory(context.dist_dir)
use_release_archive(context, archive, id = rev)
context
}
build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs, website = website)
}
}
}
diff --git a/src/Pure/System/platform.scala b/src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala
+++ b/src/Pure/System/platform.scala
@@ -1,88 +1,89 @@
/* Title: Pure/System/platform.scala
Author: Makarius
System platform identification.
*/
package isabelle
object Platform
{
/* platform family */
val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows")
val is_unix: Boolean = is_linux || is_macos
def is_arm: Boolean = cpu_arch.startsWith("arm")
def family: Family.Value =
if (is_linux && is_arm) Family.linux_arm
else if (is_linux) Family.linux
else if (is_macos) Family.macos
else if (is_windows) Family.windows
else error("Failed to determine current platform family")
object Family extends Enumeration
{
val linux_arm, linux, macos, windows = Value
+ val list0: List[Value] = List(linux, windows, macos)
val list: List[Value] = List(linux_arm, linux, windows, macos)
def unapply(name: String): Option[Value] =
try { Some(withName(name)) }
catch { case _: NoSuchElementException => None }
def parse(name: String): Value =
unapply(name) getOrElse error("Bad platform family: " + quote(name))
def standard(platform: Value): String =
if (platform == linux_arm) "arm64-linux"
else if (platform == linux) "x86_64-linux"
else if (platform == macos) "x86_64-darwin"
else if (platform == windows) "x86_64-cygwin"
else error("Bad platform family: " + quote(platform.toString))
}
/* platform identifiers */
private val X86 = """i.86|x86""".r
private val X86_64 = """amd64|x86_64""".r
private val Arm64 = """arm64|aarch64""".r
private val Arm32 = """arm""".r
def cpu_arch: String =
System.getProperty("os.arch", "") match {
case X86() => "x86"
case X86_64() => "x86_64"
case Arm64() => "arm64"
case Arm32() => "arm32"
case _ => error("Failed to determine CPU architecture")
}
def os_name: String =
family match {
case Family.linux_arm => "linux"
case Family.macos => "darwin"
case _ => family.toString
}
lazy val jvm_platform: String = cpu_arch + "-" + os_name
/* JVM version */
private val Version = """1\.(\d+)\.0_(\d+)""".r
lazy val jvm_version: String =
System.getProperty("java.version") match {
case Version(a, b) => a + "u" + b
case a => a
}
/* JVM name */
val jvm_name: String = System.getProperty("java.vm.name", "")
}