Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2016-09-21

| 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/
06:11 yaqwsx joined #divine
07:32 yaqwsx joined #divine
12:17 yaqwsx joined #divine
12:58 yaqwsx joined #divine
14:10 yaqwsx joined #divine
14:31 xstill_ mornfall: jo, tím že zařízneš ten stacktrace tak já nemám jak kontrolovat ty nechycené výjimky, protože to tam prostě není vidět
14:33 xstill_ moc nevidím důdovd do zařezávat, kromě potenciální nekonečné rekurze
14:41 xstill_ přidám zatím přepínač, který to nastaví a nastavím ho v testech
14:41 xstill_ proč verifikuješ v testech jednovláknově?
14:45 yaqwsx mornfall: u mě v homu najdeš konfiguraci faultů.
15:42 xstill_ mornfall: máš tam patche
15:42 xstill_ teď to prochází
16:24 yaqwsx joined #divine
17:44 yaqwsx joined #divine
18:12 yaqwsx Ok, jak bys to udělal tedy lépe?
18:22 evenfall asi něco jako má gcc -Wl, tzn. jednu opšnu která uvozuje něco co se pak pošle dios-u
18:23 evenfall jinak se to bude hrozně prát, když tam mají přijít nastavení verifikátoru (--threads), nastavení dios-u, nastavení překladače
18:24 evenfall ještě mě teda úplně netěší to #include "..." (zejména #include "../dios.h")
18:25 yaqwsx Fakt? Já osobně to spíše preferuji (navíc v dios.h je to třeba, aby se dal includnout do UI)
18:25 evenfall ono taky to #include <runtime/dios.h> v divinu je takové nešťastné
18:26 yaqwsx Ok, tak pokud bychom zmněnili to rozhraní a string by si parsoval až DiOS, tak to může zmizet...
18:27 evenfall ne že by dios nebyl aktuálně to jediný co v divinu umíme nabootovat, ale stejně bych radši držel nějakou separaci
18:28 yaqwsx Dává to smysl. Jak si tedy představuješ to command line rozhraní? Patche stáhnu a klidně to předělám.
18:29 yaqwsx Ale chtěl bych mít asi nějakou lepší představu, jak to má vypadat.
18:29 evenfall to asi hlavně záleží na dios-u, resp. jaký typy nastavení by měl mít
18:30 evenfall jedna možnost by byla -o {string}, případně -o {string} {string}
18:30 yaqwsx Respektive otázka - z pohledu UI, rozlišovat mezi faulty a selháváním mallocu?
18:30 yaqwsx *selháváním např. mallocu?
18:31 yaqwsx Aby to bylo univerzální (a použitelné i mimo DiOS), tak bych tedy asi zavedl něco ve stylu -ostring=string nebo -ostring string
18:32 yaqwsx Abych např. faultu konfiguroval ve stylu -ofault.arithmetic=enabled,override
18:32 yaqwsx Je to ale celkem ukecané.
18:32 evenfall jo no, na faulty se tam to = zrovna moc nehodí
18:33 evenfall -o ignore:arithmetic -o report:memleak -o continue:memleak?
18:33 evenfall s čárkama se to bude zase blbě parsovat
18:34 yaqwsx To vypadá dobře. U faultu ale chci specifikovat tři věci - zapnut/vypnut, pokračovat/nepokračovat, povolit/nepovolit programu měnit nastavení faultu
18:34 yaqwsx Bude se to blbě parsovat? Tady na to parsování by nemuselo vadit zatáhnout do DiOSu STL, když se provádí stejně jenom na začátku, ne?
18:35 evenfall nevadilo, ale furt s tím je víc práce
18:35 evenfall jsem myslel že se tam stl už stejně objevuje
18:36 yaqwsx V minimální míře - std::array, std::pair a std::tuple
18:36 evenfall ještě jedna možnost by byla mít jiný uvozovátko než - pro dios
18:37 evenfall možná + je nejlepší :)
18:37 yaqwsx Moment, já vlastně čárky nepotřebuji - když se to udělá, jak říkáš ("příkaz" první, argument druhý), tak to můžu libovolně naspecifikovat
18:38 evenfall jo to jo
18:38 yaqwsx Ok, to se mi libí - předělám.
18:39 evenfall která možnost?
18:39 yaqwsx -o ignore:arithmetc -o report
18:39 yaqwsx :memleak
18:39 evenfall no furt je na stole to + :)
18:40 evenfall ale možná je to už trochu divoký
18:40 yaqwsx Jakože "+ignore:arithmetic +report:memleak"?
18:40 evenfall tzn. všechno s - parsuje divine, + přeposílá dios-u, všechno za zdrojákem/binárkou jde programu
18:41 yaqwsx Až takhle? Není to moc divoké?
18:41 evenfall možná je
18:42 evenfall tak asi -o {string}
18:42 yaqwsx Na druhou stranu - rozdíl mezi + a -o je minimální a předělat je otázka 5 minut.
18:43 evenfall ne tak docela
18:43 yaqwsx Tak pak asi nevidím - myslel jsem, že option v UI umí namatchovat cokoliv.
18:44 evenfall to jo, ale ten parser by musel být v divine/ui ne v diosu
18:44 evenfall určitě by aspoň divine musel vědět že za +e má jít string kterej ještě patří k tomu +
18:44 yaqwsx Jakto? Proč nemohu "-o {string}" nebo "+{string}"?
18:45 evenfall jo takhle :-)
18:45 evenfall jo to jo
18:45 evenfall já si představil 5 minut od toho jak to vypadá teď, tak jsem to pochopil tak že bys přepsal -e na +e :-)
18:46 yaqwsx To 5 minut nebude :D
18:46 evenfall mezi -o {string} a +{string} skutečně rozdíl není
18:46 yaqwsx Ok, tak už si rozumíme.
18:46 yaqwsx Zkusím to zítra v mezerách mezi cvikama překopat.
18:47 evenfall fajn, já budu taky víceméně na FI
18:47 yaqwsx Jen pro jistotu, ať nelituji - patch zruším z historie, ale ponechám ve working directory pomocí unrec, že?
18:47 evenfall ano
18:47 yaqwsx Ok, dík
18:49 evenfall xstill_: k --threads 1, aspoň teď jsou ty testy skoro všechny sekvenční a tam --threads ničemu nepomůže
18:49 evenfall xstill_: teda větší
18:49 evenfall xstill_: stejně nemůžeš generovat najednou víc než jeden další stav
18:50 evenfall navíc maj často něco jako 2 stavy
18:54 evenfall (no a když se někde něco rozbije, tak je lepší když tady ty testy produkujou v každým běhu stejnej výstup, to s více vláknama fungovat nebude)

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