[isabelle-dev] mira disk usage

Sat Sep 1 01:15:17 CEST 2012

I guess the problem is that build -b produces heap images for all sessions. These are many, and each image is hundreds of MB. The previous setup had images for selected base sessions only and no images for the rest (almost everything).

I've had the impulse before to try and select only a set of sessions for image building. This doesn't seem possible with one isabelle build invocation and I'm not sure we want to complicate the command line interface further by trying to have some selection syntax on that level.

Would it be a viable alternative to control image building via an option in the ROOT file? That would still allow command line override, and could use the standard options interface for defaults etc.

Gerwin

ps: "isabelle build" takes about 5 sec on my system to figure out dependencies (I think). Should this be faster?

On 31/08/2012, at 7:38 PM, Lars Noschinski <noschinl at in.tum.de> wrote:

> On 29.08.2012 20:29, Florian Haftmann wrote:
>> Hi Lars,
>> 
>>> Most space seems to spend with Isabelle_makeall and AFP runs, amounting
>>> to 4-5GiB each. Has someone an idea what changed?
>>> 
>>> If yes: do we want to revert to store less stuff again or should we
>>> implement some kind of automatic cleanup?
>> 
>> can you provide us with a du dump or something like that?
> 
> After my last mail, I deleted all but 25 runs. No we are back 133 runs, occupying a whopping 316GB; this stems almost exclusively from the heap images (the log files are 135MB, and the classes 2GB).
> 
> In the output below, the two classes of AFP runs are for different polyml setups: polyml-5.5.0_x86-linux for the smaller and polyml-5.4.1_x86_64-linux for the bigger.
> 
> $ du -s * | sort -n
> 41080   Pure_7ff7454fb4a949e0b2af2acd669f9b1b
> 41080   Pure_b140a895004c40e1b01f7cc21645eef3
> 41080   Pure_b384d445f0ae4ff5af810afadaec37f1
> 41084   Pure_4f9a65b8defc44b48c05e813a9999f89
> 41084   Pure_9bb68cd8a5684146af13bb0e33427db7
> 41092   Pure_0755a3845e304148aeb7348179f90ac8
> 41092   Pure_07ada386ea2d45e9a3d4583a447b539b
> 41092   Pure_6faf9c35a41c430198aaea739e1037af
> 41092   Pure_70b3a7f6eceb44dc9f911ce565d20d94
> 41092   Pure_8c960375e94742cc9fd8c32fc863fcf4
> 41092   Pure_90f6a492ab8e46f888dd1667c5f78eb2
> 41092   Pure_98c579af29c14640bd6febd613fc334b
> 41092   Pure_b4234fdb24a44d7d9c0c71fab693d2c6
> 41092   Pure_bb3d8bb1963e48999d38ec788b90976c
> 41096   Pure_3117b446d69f4fb0830d4038d73fc4d1
> 41096   Pure_abf3b1415a994d7c88348bbf4618e710
> 41096   Pure_be6f8f4f9ae9401eb861de7ceff2fd66
> 41096   Pure_eac116c893fa4d8f982911acf87c71b0
> 41096   Pure_f8ebc4fbbbc6411d8e0a764aac97421c
> 41116   Pure_10ac9eb730794cf086d045ad5799e90a
> 41116   Pure_20a9c663756140f29d2a7f54255c4c06
> 41116   Pure_2274de0a74364eb68dd20899311953df
> 41116   Pure_416a99887b1045f5b428081d96415e48
> 41116   Pure_686572d8e2264936be876f3744983b2b
> 41116   Pure_bc456446be8447fa98145482d09789cd
> 41116   Pure_ded21929ceba41c5bfcabbf0ef844cc1
> 41116   Pure_e38bd7a81e604784becfe3f6a1d317ca
> 188156  HOL_5301cc2530b44f3c8fbaab6631649625
> 188160  HOL_bb50ae005fce4f169e567555aa7086e3
> 188164  HOL_4ffe7e2bd8634ca4ac53f61f5e9b8d8b
> 188164  HOL_b172004bc51d4204930d707ade2a9948
> 188168  HOL_32dd28cc9837431a9258808b60bb929d
> 188176  HOL_25d2e31db5ad49e2b31ddcf20240fc1a
> 188184  HOL_c09f7799000240819920c73c6277f3b6
> 188188  HOL_a67d5e4912124edcb4d555255638ed0a
> 188192  HOL_979c9a0b33e74059b589afb7ea2ae569
> 188204  HOL_38279c994df24bc2a45074a08af74ce1
> 188204  HOL_3924edbd4141442382a3002e158ea0cb
> 188208  HOL_22115dcdf17e4f5d8fd97b6b01d34525
> 188208  HOL_67e5642661104034b1b0a233ee9dfa10
> 188208  HOL_b3197b6a623345b8b56dcf0db27dad3c
> 188212  HOL_d5dae0d91d784b9689a567eb0b62c01d
> 188216  HOL_323189482d52489ba42096af3813ee70
> 188216  HOL_33fb87457daf46f1887e0326e2f23893
> 188232  HOL_561aa019ff40495f921ac8993f3bc993
> 188240  HOL_94b1210217c34bc4a78f24fae7fdbdbb
> 188268  HOL_2b6c8c82e5744621b7c9ba4f46318f01
> 428632  SML_HOL_43ada5d848674748a280aa664d9c0df6
> 428640  SML_HOL_2a145caa67244d6495840e2e71f52a1f
> 428640  SML_HOL_35743e23f67447a7aefc528297cc1a30
> 428640  SML_HOL_74c3673325904603b3bd7d9b7df10d02
> 428644  SML_HOL_92e4bd3d450345ff9b2b17b9252a2a64
> 428648  SML_HOL_03489de971214c5ba756c9fd69a1a174
> 428652  SML_HOL_7c9d988abc544a33af19e1a1789d7ad5
> 428652  SML_HOL_841a812b911c4fdebe71ad11ef936870
> 428660  SML_HOL_acbd40734a1e460393834994fba550a3
> 428668  SML_HOL_73fe342e44f843a1b701fd9781cee328
> 428672  SML_HOL_ab7a82693cb046bdacef9ea097022219
> 428680  SML_HOL_7429eef2bea4490ea9c885992b182b73
> 2648788 AFP_a493d4174cb645aea6b9d2f85177370b
> 2649016 AFP_d34612e9548c4676957da807b824790a
> 2649260 AFP_03714526f60e41e5ba96206c0eb1bb99
> 2649320 AFP_b471a04e2c984afa82fd144537a80d39
> 2649476 AFP_5997d13453fb47e4ab95933f327e0465
> 2649660 AFP_5848988b8ced4af59b7423feabf3f373
> 2649764 AFP_55670b4c356e44d59b917225f73d6dc2
> 2650012 AFP_81d7c8a1afc348aaaf3ceffd7bd24b5c
> 2650056 AFP_d4a95ee25b2f4d09b1c036f58a1925f2
> 2650088 AFP_7cec58ab1b514f1c86dab5171fc9510c
> 2650224 AFP_acb2e5d7e0884df192250e84c125833e
> 2650264 AFP_e36b9541d224415d82fcb6d7c835e93e
> 2650336 AFP_e3c20912d59d45ea97c02dd1fe41581b
> 2650380 AFP_f77015feaed743469636ccc1f8cb0464
> 2650504 AFP_e2bb9f65b16a419ab02b0033c0cdabca
> 2650752 AFP_61d4c33f2c0e41269d8f3d815ade50dd
> 2658640 AFP_2018d9c8100b498a9d89298945a9d762
> 4277552 Isabelle_makeall_8658cfd9cf2e41d2b2ec7f31257c5a10
> 4277712 Isabelle_makeall_f79d72e7ca1440e9a12273a6bd116954
> 4277720 Isabelle_makeall_37cb8966f23a49e8a81fc079334d7e34
> 4278052 Isabelle_makeall_c9c7f96e5dca4ba9a51f83ac924e34a2
> 4278644 Isabelle_makeall_9cd33fa6f6604740a5cfae961f4fc1b8
> 4278952 Isabelle_makeall_6170418d7dd842e0a97e3909ec6fe434
> 4875244 Isabelle_makeall_5350aec3718d48f2a4c241a2046fa32c
> 4875736 Isabelle_makeall_1dc5b832eca14b7d9b61ca9a90933b3c
> 4875776 Isabelle_makeall_5d09c5dd58e740f18a9703decb668ce2
> 4876036 Isabelle_makeall_6881b958a16648768e67768141a60234
> 4876044 Isabelle_makeall_862590bd298944efbe34e97e0c03492e
> 4876228 Isabelle_makeall_557378a0a2204151abcca2bff5fc16b5
> 4876316 Isabelle_makeall_6a4bb82d50524a9e9616e5a7017d6051
> 4876316 Isabelle_makeall_f2bd7c930f4d48b590af6fe2c1bb64d4
> 4876360 Isabelle_makeall_202048c010664589b5512ba175d41db6
> 4876464 Isabelle_makeall_2f06bf59dae0476fbc21ee27538576b4
> 4876704 Isabelle_makeall_0d0f82e40bf844049e8ecc2dfa0fd590
> 4876740 Isabelle_makeall_ce7f359ca73545da8835f78c4d1323a1
> 4876804 Isabelle_makeall_55a690b672ff4110b9629a6a9a7c14c4
> 4876832 Isabelle_makeall_743603005aa4405899175ba5ba405061
> 4876884 Isabelle_makeall_c2ee7fe9cf0447b8a0236e3a4e301e15
> 4876908 Isabelle_makeall_35c4a36c71d54225b6e44c415e61e76f
> 4877008 Isabelle_makeall_c878eb4bfa9e4f7e94ac158cd29d6b2f
> 4877024 Isabelle_makeall_804d74bae1884012a28193d7d121ce0b
> 4877136 Isabelle_makeall_ca7349cdc27845939702c7351d6f1132
> 4877156 Isabelle_makeall_96d38857233f481e85c1adaaec95fd89
> 4877344 Isabelle_makeall_f727d29f2c2741afaeb7e3a9cf421d8e
> 4877348 Isabelle_makeall_9d641b4d68f54c86ad9e6b471185a748
> 4877476 Isabelle_makeall_7a2ef5e5ec7f4d40b6a57c3aab3fa2a5
> 4877640 Isabelle_makeall_53904095274249f39fcd181f2fb8574f
> 4877664 Isabelle_makeall_432914b0a0ee43f1b3534bcfea601f37
> 4877772 Isabelle_makeall_217c8b5403e94cba952b32c94451b482
> 4877848 Isabelle_makeall_5309213b60154931b4bda7cd478337ce
> 4878356 Isabelle_makeall_757f5654687f43ed86b8e86df87d0dba
> 4878460 Isabelle_makeall_053e771e049e402e8a91ca3fc5bf0590
> 4892556 Isabelle_makeall_8decfe43116044e9b4b9d0f99307c566
> 4948140 AFP_b849d19028b64acd9b8ce7e61f62c139
> 4948336 AFP_0be37a590ae54e90b43d6bad01484a69
> 4948640 AFP_a2d11fc89d914610921d8f38822874a3
> 4948704 AFP_d3f02605e1444269bc9746e45b8ab146
> 4949432 AFP_34e7da1f5a874853befbbbeaf5951c63
> 4949436 AFP_3ef5133f8ecb4636bb40638d506b5859
> 4949696 AFP_70f1497842c64b73bd9133f904ced851
> 4949780 AFP_d27626a276864b49822c16726eda111c
> 4950024 AFP_47bdcbd2519b46249830703afbcfaf50
> 4950028 AFP_ed82c83c040b4a30b30b3d4787f301bd
> 4950384 AFP_5500ff011c4a4f3d8d195998dbd78d9e
> 4950484 AFP_8ea0e83d849a43d0854e29f548971c76
> 4950584 AFP_660a7ec5412f43b9b23306ae81a53378
> 4950788 AFP_d264d239be4749599d9a04ed9655743e
> 4951044 AFP_06afd3a579c4400bbd8d0536d2613b59
> 4951220 AFP_d5661d784ad44def87f23b32f62cb8ad
> 4951676 AFP_fcdb0a02432d41e1949e2312fc27b0f0
> 4951740 AFP_bd5afcfc8bbb4619bc7d1264aa1b170c
> 4951820 AFP_2f4bf9b180824c6c88e6bd55ff811d67
> 4951904 AFP_1123ab8e31a44ffdad06b49fd2c80192
> 4952268 AFP_752bcfc9c7d94cafa9cdd9acdf97968f
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 