Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2016-06-19

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #divine
01:48 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
11:42 xstill mornfall: v mém branchi máš nějaké patche
11:50 xstill mornfall: krom toho by ses mohl přihlásit na https://gitlab.fi.muni.cz a podívat se na https://gitlab.fi.muni.cz/paradise/DIVINE/issues konkrétně #14, #3, #5 a #10 -- jsou to návrhy na témata ze kterých by si Katka mohla vybrat bakalářku, prioritně bych je seřadil v tom pořadí, které jsem psal. Takže pokud k tomu máš nějaké připomínky, nebo návrh na něco dalšího, tak teď by to
11:50 xstill bylo vhodné…
12:29 xstill předpokládám, že s kompilací libunwind v DIVINE jsi nic nedělal?
14:51 xstill btw. když teď máme kompilátor pod kontrolou, nezapneme si c++1z?
16:48 mornfall #14 je na bakalářku pravděpodobně dost triviální (jestli fakt jde jen o to vytvořit 3-4 aliasy, který se každej přepíšou na noop nebo na __vm_mask a na pár místech je zavolat)
16:48 mornfall #3 je na bakalářku zase docela moc
16:49 mornfall #5 je OK, #10 mi přijde hodně málo užitečný
17:05 mornfall (pokud jde o Viki, přijde mi dost uhozený dávat ji něco čemu v labu nikdo nerozumí, zejména po nedávném velkém úspěchu s Kristýnou)
17:36 xstill to není úplně domyšlený o co jde v 14, nicméně asi máš pravdu, že by to mohlo být moc lehký; uvažoval jsem, že by to měl obashovat i vytvoření sady benchmarků. O tom, že je #3 těžká vím. #5 může být taky relativně jednoduchá, ale snad OK. Proč ti #10 příjde až tak neužitečná?
17:36 xstill bavil se s tebou Jiřík o Viki?
17:37 mornfall nebavil, potkal jsem Heňa
17:38 mornfall no, máme nějaký programy který používaj win32 vlákna a chceme je verifikovat?
17:39 xstill aha… ale teda přibližně informovaný jsi? Máš nápad na něco spíš teoretického co by bylo užitečné pro DIVINE a mohla to Viki dělat?
17:40 xstill nemáme teď, ale ne že bychom měli celkově přebytky programů na verifikaci…
17:40 mornfall tak jinak, kolik programů znáš který win32 vlákna používaj? (starej divine se nepočítá)
17:41 mornfall nebo ještě lépe, který používaj win32 vlákna a neumí používat posixový
17:42 mornfall (já jich sice pár znám, ale ani k jednomu z těch co znám neseženeš zdrojáky)
17:42 mornfall jakože určitě je hodnota to umět, ale někde v posledním půl procentu věcí který potřebujem aby byl divine 'úplnej'
17:43 xstill hm, dobrej point; jakože neznám žádný, což ale přičítám spíš tomu, že jsem se o vlákna začal zajímat v podstatě až v době když jsem používal linux
17:46 mornfall zhruba každej program kterej umí vlákna jinde než na windows (typicky to pro vláknovej program je to stejný jako 'jde spustit') umí posixový, a win32-only aplikací který bychom chtěli verifikovat moc není (MS Exchange a MS IIS asi, ale viz problém se zdrojákama)
17:46 mornfall (pro zajímavost, MS SQL je nebo brzo bude ve verzi pro Linux, takže umí posix thready)
17:48 mornfall a pak teda množina programů který potřebujou z win32 jen ty vlákna a nic jinýho je taky plusmínus prázdná, takže aby to k něčemu bylo, tak to znamená implementovat toho ještě mnohem víc
17:48 xstill ok, tak win32 thready ne
17:49 xstill napadá tě něco pro tu Viki?
17:49 mornfall jinak teda #3 by šlo klidně rozdělit na teorii a implementaci a tu teorii by Viki asi dělat mohla, resp. sice o tom toho víme dost málo, ale nesrovnatelně víc než o diferenciálních rovnicích
17:51 xstill hm, to mě nenapadlo
17:54 mornfall (popravdě se myslim, že kdyby si s ní někdo sedl, tak by zvládla klidně i bakalářku s implementací, teda ne #3 ale něčeho menšího... ale počítám že si sama řekla že programovat nechce, ani sama ani s někým?)
17:56 xstill nevyloučila, že by něco naprogramovala, ale nechce práci ve které by byla implementace nějak velká část
18:02 mornfall druhá věc která by mě zajímala (to jsem shodou okolností říkal aj Heňovi) by bylo CTL*, kde by zadání mohlo klidně být najít/vymyslet algoritmus, plus minimální sekvenční implementace třeba
18:09 xstill tam mám trochu problém, že jsem hrozně neinformovanej o tom co vůbec existuje a co z toho by se případně dalo udělat v našem prostředí
18:32 mornfall zase je to bakalářka, tam je průzkum literatury docela validní výsledek sám o sobě
18:36 mornfall může třeba zjistit, že nejlepší známý algoritmus dělá nějaký průchody, že to je ve spojení s našim pomalým generováním následníků problém, z nějakých známých dat odhadnout kolik paměti by stálo pamatovat si (aspoň část) hran a kolik času by to ušetřilo...
18:37 mornfall neříkám, že by nebylo lepší to implementovat a vyhodnotit tak, ale stačilo by to i bez toho (a ta implementace by nemusela být ani tak těžká nakonec)
18:48 xstill_ joined #divine
18:51 xstill dobře
18:52 xstill to dává smysl
18:57 xstill mornfall: ještě teda jednu věc Jiřík zmínil jen přede mnou, a to že by teoreticky Viki mohla navázat na to co dělala Eva a Maja u Ivany
19:05 mornfall to by určitě mohla, jen nevim proč Jiřík furt odhání studenty od divinu
19:06 xstill to nevím
19:20 xstill jen vím že má pocit, že implementačně je divine hrozně složitý pro novýho člověka
19:21 xstill nebo teda alespň takovej dojem z něj mám
19:32 mornfall jo, cestou do Berlína v 2007 jsme to hodně řešili
19:33 xstill heh, tou dobou jsem byl v druháku na střední :-D Co jste tam vyřešili?
19:35 mornfall nic, že programuju moc složitě a já se jim snažil vysvětlit, že abstrakce je základní programátorský nástroj a nějak to nechtěli pochopit (a řekl bych že dodnes nechápou)
19:39 mornfall nakonec to byl vlastně stejnej problém jako naposled na sprintu
19:40 mornfall oddělil jsem procházení grafu od zbytku algoritmu a Jiřík z toho doteď nemůže
19:49 xstill hm, já souhlasím s abstrakcí, zas na druhou stranu chápu, že to je těžké se tím prokousat, obvzlášť když do toho přicházíš malou znalostí jazyka. Mě s Jirkou to taky trvalo dobře semestr než jsme pochopili část divine. Jakože ono to nakonec stojí za to, jen musíš být schopný do těch lidí investovat víc asistence na začátku.
19:51 mornfall lab zase nebyl nikdy koncipovaný jako rychlovarka na bakalářky, takže nějakej semestr seznamování je nejmíň
19:53 xstill jojo, problém může být, že Jiřík je teď spíš ten kdo by se potřeboval seznamovat, ale vedení bakalářky ho staví do situace kdy se od něj očkává, že bude pomáhat těm studentům v seznamování se…
19:57 mornfall jo, ale když chci to seznamování nějak zorganizovat, tak to nepřichází do úvahy
19:58 xstill tím teď myslíš co?
20:02 mornfall no třeba sprint (to bylo furt jen jak něco nejde) a když jsem se jen opatrně zeptal na pravidelnej divine v semestru tak to byla hned pohroma
20:02 mornfall přitom je X možností jak to aspoň zkusit podpořit a ne to paušálně utopit jako nereálný
20:03 mornfall je to celý boj s větrnými mlýny
20:05 xstill no však jsme to neutopili, ale musíš zas pochopit, že těžko lze vznést požadavek na to aby lidi neměli narozvhovaný přednášky a cvika v době kdy chceme DIVINE. A občas jsou přednášky na který člověk musí/chce chodit, takže ti nejde dát garanci, že budeme mít všichni vyhrazený čas.
20:09 mornfall no, o moc víc utopit už to asi nešlo (jedině snad to rovnou radši zakázat)
20:12 xstill a co jsme s tím podle tebe měli dělat? Pokud vím, tak jsme se shodli, že se budem snažit si nechat volnou středu
20:23 xstill jinak, http://www.sciencedirect.com/science/article/pii/S1571066105001714 vypadá to, že dokonce už i paralelní CTL* bylo (přes alternující automaty). Otázka by teda spíš byla jak to zapojit do našeho systému, kdy ideálně chceme zapojit tu CTL* formuli dovnitř modelu
20:25 xstill a probrat se těma algoritmama teda
20:32 mornfall no asi nic, prostě to nejde, když už to musí být tak teda jsme ochotní se ve středu sejít, ale rozhodně nikdo nic neslibuje, protože ani pro kmenové vývojáře v divinu to vlastně není priorita (a když jsem to kdysi nějak prosadil a náhodou se to povedlo zorganizovat tak to nemělo žádnej přínos, tak proč se snažit)
20:37 mornfall nikdy jsem neřekl že všichni studenti musí celej den mít volno a že nesmí na přednášku, ale s trochou domluvy napřed a s trochou spolupráce od Jiříka by určitě šlo zabezpečit docela slušnej společnej prostor
21:24 mornfall docela mě ale mrzí, že máme celkem unikátní šanci rozjet smysluplnej projekt s redhatem a zatím děláme všechno pro to aby se to co nejdřív rozpadlo

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary