Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-11-16

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

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #divine
02:47 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
09:28 spito joined #divine
09:29 spito Nějaký nápad, proč padá test dve/commit?
09:31 mornfall hej fakt nevim, je to nějaký pošahaný
09:32 mornfall protože valgrind: m_debuginfo/image.c:465 (set_CEnt): Assertion '!sr_isError(sr)' failed.
09:35 mornfall ta stejná binárka na antee ale funguje
09:38 mornfall ten lcov je jinak neškodnej
09:39 mornfall aha, no
09:41 mornfall arke zase jednou vykapala
09:41 mornfall (disk)
09:46 mornfall hmm, a teď fsck na /nix-u
10:06 mornfall ok, arke nějak funguje
10:09 xstill co si s tím provedl?
10:09 mornfall s čím?
10:09 xstill arke
10:10 mornfall power cycle
10:10 mornfall vypadl disk zase
10:10 xstill aha
10:11 spito joined #divine
10:12 spito mornfall: na to s tím valgrindem jsi přišel jak?
10:12 mornfall to byl problém s diskem
10:14 mornfall [ 0:02] terminating with uncaught exception of type brick::_assert::AssertFailed: /tmp/nix-build-divine-clang_medium_debug_x64-3.2.0+pre5372.drv-0/divine-3.2.0+pre5372/divine/utility/output.h: 22: assertion `!!_output' failed;[ 0:02]
10:15 mornfall hm, že já se díval do release buildu předtím
10:15 mornfall (kde to segvilo)
10:16 mornfall spito: řekl bych žes to rozhasil
10:17 spito dík
10:18 spito dobrý vědět
10:19 spito (snaha dostat se na hydru končí na 502 - Bad Gateway)
10:19 mornfall jo, to je systemd
10:20 spito nojo, dobře, rozhasil jsem to
10:20 mornfall polovinu služeb musím nahazovat po rebootu ručně
10:20 spito ale jakto, že u mě to funguje
10:33 spito mornfall: a můžu si nějak přečíst, proč ten který test spadnul
10:37 mornfall [details] žejo :)
10:48 spito hmm, a to najdu kde? (netrollím)
10:49 spito v Summary nic takovýho není
10:49 spito a Details vedle Summary mi nic neřekne
10:52 xstill na status stránce je nahoře vpravo takové nenápadné [details]
10:53 xstill a tak se pak dá rozkliknout test
10:53 xstill a teda nevím kde zas bereš to summary
10:54 xstill a teda hlavně asi tenhle status: http://divine.fi.muni.cz/status/status?project=divine&branch=mainline
10:54 xstill mornfall: bylo dobré kdyby se na něj dalo někak proklikat
10:58 spito xstill: všechno z hlavní stránky http://divine.fi.muni.cz/status.html
10:58 xstill no odtamtut se na to správné právě proklikat nedá
11:03 spito no a to je špatně, žejo
11:03 spito btw: je toto validní DVE? '1->2 1->3 2->4 3->5 3->1 4->6 5->7 7->8'
11:04 * xstill neví jak vypadá validní DVE
14:35 mornfall spito: v jakým smyslu?
14:35 mornfall to je výstup z draw (zesedovanej)
14:39 mornfall každopádně vim proč to padá :-) jen nevim jak to opravit
14:40 mornfall vlastně vim
14:40 mornfall to je totiž zase ten unique_ptr :P
14:41 mornfall hmm
14:41 mornfall ale já si stejně nepomůžu
14:41 mornfall každopádně problém je že aj statistiky aj output jsou unique_ptr
14:41 mornfall statistiky používaj output
14:41 mornfall ale nikdo nikde nezaručí že se destruktory zavolaj ve správným pořadí
14:51 mornfall no, snad jsem to vykoumal
15:29 xstill mornfall: je reálistický řešit fairness tak, že bysme byli schopní nějak anotovat nonprogress cykly a pak bysme dovolili jen takové cykly, které a) obsahují progress hranu, b) nelze je opustit progress hranou
15:29 xstill pak by totiž mělo jít detekovat livelocky v LLVM pomocí LTL
15:32 mornfall jo, detekce non-progress cyklů by fungovala, pokud dokážeš rozlišovat progress/non-progress hrany
15:33 mornfall to říkám pořád ne? :-)
15:33 mornfall ten problém není najít cykly, problém je vyřešit to značení
15:34 xstill no muselo by se to udělat nějak aby se to dalo označit ve zdrojáku
15:37 mornfall no, a taky aby to nebyl opruz :)
15:38 xstill to právě nedokážu až tak odhadnout nakolik by to byl opruz
15:46 spito mornfall: #pragma bolí?
15:46 mornfall spito: v jakým kontextu?
15:46 spito poznačení ve zdrojáku
15:48 xstill no problém je spíš to, že celkem cokoli bude bolet pokud bys to kvůli verifikaci musel napsat ke každýmu druhýmu cyklu, ale myslím, že tak zlé to nebude
15:48 mornfall no, #pragma jako progress je úplně k ničemu
15:49 xstill no značit progress je celkově dost k ničemu, proto jsem říkla značit nonprogres cykly, těch není tolik
15:49 xstill protože málokterej cyklus ve zdrojáku ti reálně dělá cyklus ve stavovém prostoru
15:50 mornfall jo takhle... tak tohle nefunguje
15:50 xstill proč?
15:50 mornfall hrana ve stavovým prostoru je složení hran ve vláknech
15:50 mornfall co je progress+nonprogress?
15:51 mornfall i když možná by to tak nevadilo
15:51 xstill no progress, ne? Pokud teda myslíš jako že "najednou" táhnou dvě vlákna a jen jedno je progress
15:52 mornfall jen teda ta detekce bude bolet
15:52 mornfall protože hledáš cykly který maj nonprogress hranu v každým vlákně
15:53 xstill teď to asi nechápu
15:54 mornfall no, non-progress cyklus ve stavovým prostoru je takovej (pokud značíš non-progress hrany) kterej má v každým vlákně non-progress hranu
15:54 mornfall hm
15:54 mornfall nebo aspoň v jednom?
15:55 mornfall ta inverze je trochu problémová :-)
15:55 xstill takovej co má jen non-progress hrany, ne?
15:55 mornfall to určitě ne
15:55 mornfall to by fungovalo kdybys značil progress
15:57 mornfall LLVM se chová tak že nikdy nedokážeš zaručit že ti někam nevklouzne neoznačená hrana
15:58 xstill mám v tom bordel, moje představa byla, že by se anotoval cyklus a to by znamenalo, že všechny tahy toho vlákna kde PC je uvnitř toho cyklu by byli nonprogress
15:58 mornfall co je to cyklus?
15:58 xstill teď jsem myslel cyklus ve zdrojáku
15:59 mornfall otázka furt platí :-)
15:59 xstill jako while (otázka je co s tail-rekurzí)
15:59 mornfall a s goto
15:59 xstill tak, to že bys nemohl anotovat goto by asi až tak nebolelo
16:00 xstill kdo dneska píše cykly přes goto
16:00 xstill a chce to verifikovat
16:00 mornfall no, ber to tak že překladač cykly přepisuje na goto
16:00 mornfall takže co přesně z toho vznikne těžko říct
16:00 mornfall jako je v bitkódu moment kdy existuje nějaká struktura kolem cyklu
16:01 mornfall ale pochybuju že je zaručený že se zachová až k divinu
16:03 xstill no dobře, tuhle část domyšlenou nemám
16:04 xstill ale kdyby byly takle ty cykly ve zdrojáku označený, tak pak by nonprogress stavove cyklus byl jen ten s všema hranama nonprogress, ne?
16:06 mornfall já nevim
16:06 mornfall to asi záleží co od toho chceš
16:06 mornfall pokud máš nějaký služební vlákno který čeká na request a zbytek systému je v livelocku tak to tenhle postup detekuje jako progress
16:14 xstill no to záleží jestli čekání na request je progress
16:14 mornfall no, zejména to nemusí být cyklus ve zdrojáku
16:18 xstill tak čekání vždycky bude nakonec nějakej cyklus
16:19 mornfall nakonec jo, ale ten cyklus může být docela netriviální
16:19 mornfall jako while ( true ) check(); kde check je složitý
16:23 xstill to by samo ani nevadilo, pokud bys mohl to nonprogress označení spojit i s celým tím check(), (možná podobně jako dneska interrupt_mask)
16:28 xstill tj., že by se ti [[noprogress]] while ( x ) { y; } muselo přespat na __divine_noprogress_begin(); while ( x ) { y; } __divine_noprogress_end(); což má teda nevýhodu, že bys nějak musel být schopný manipulovat s frontendem což by mohlo bolet
16:29 mornfall to hlavně nebude fungovat
16:29 mornfall nebo nevim
16:29 mornfall pokud to bude dědičný jako atomic tak možná jo
16:29 mornfall ale i tak je to hodně ošemetný
16:31 mornfall no a takhle
16:31 mornfall pokud uděláš tohle, tak to vlákno nebude nikdy generovat žádnej progress (ani když zrovna něco dělá)
16:35 xstill jo to je problém
16:36 mornfall to můžeš zase řešit tím že vyrobíš __divine_progress() ... ale to se v podstatě vracíme ke značení progress hran
17:11 xstill hm, nemohl by test-brick být k dispozici ale nepřekládat se při normálním překladu divine?
17:12 mornfall nějak to asi udělat jde
18:25 xstill spito: kde si našel tu informaci, že argumenty konstruktoru s {} se vyhodnocují vždy v pořadí?
18:34 xstill hm, může něco nebýt ani rvalue ani lvalue?
18:34 mornfall void :-)
18:35 xstill jo, a něco jiného?
18:35 xstill = něco co můžeš předat do funkce jako parametr
18:37 mornfall předat můžeš jen něco co je rvalue ne? rvalue znamená že to jde číst
18:37 mornfall http://stackoverflow.com/questions/3601602/what-are-rvalues-lvalues-xvalues-glvalues-and-prvalues
19:58 xstill hm, sakra chtěl jsem si jen trochu procvičit práci se šablonama a zabil jsem 3 hodiny programováním předávání tuple jako parametrů do funkce
20:11 spito xstill: netuším, ale někde na stackoverflow
20:12 spito nebo na cppreference
20:12 spito a nebo na wiki
20:12 spito nebo tak nějak
20:13 xstill :-D
20:13 spito http://en.wikipedia.org/wiki/Variadic_template
20:14 spito hint: hledej třídu pass
21:10 spito http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2012/n3485.pdf stánka 201
21:10 spito odstavec 4
21:11 spito poznámka: ve VS 2013 a GCC <4.9.1 to je rozbité
21:11 spito takže se to stejně nedá použít
21:11 xstill co to je?
21:12 mornfall o čem je tady řeč? :)
21:12 xstill spito: jo a dík za ten pass
21:12 spito "spito: kde si našel tu informaci, že argumenty konstruktoru s {} se vyhodnocují vždy v pořadí? "
21:12 mornfall jo tak
21:12 spito ale hledá se to fakt blbě
21:13 xstill aha tys mi našel přímo standard :-), dík
21:13 spito ...když neumíš anglicky...
21:13 spito tak...to není standard, ale draft
21:14 mornfall on v tom není moc rozdíl
21:14 mornfall naštěstí
21:15 xstill a jakto, že je to rozbitý? To si jako gcc dělá to pořadí jak se mu zachce?
21:16 spito http://gcc.gnu.org/bugzilla/show_bug.cgi?id=51253
21:18 xstill ach jo, že jim to tam leželo dost dlouho (dneska už jsem se na gcc jednou naštval protože 4.8 neumí auto lambdy ani auto návratový typ funkce)
21:19 xstill sem měl takovou slabou chvilku a přemýšlel jsem jestli už nenastal čas přejít na -std=c++1y, ale nenastal :-(
21:19 spito a teda, je fajn, že clang to umí dobře
21:20 mornfall myslíš c++14 ne? :)
21:20 spito mornfall: (já jsem myslel ještě tu věc s těma složenýma závorkama)
21:20 xstill tak pokud bysme chtělo kompilovat i něčím jiným než clang 3.4 tak 1y, ale vzhedem k tomu, že ani gcc 4.8 nic zajímavého neumí tak je to jedno
21:21 mornfall no, ono typicky dokud se to jmenuje 1y tak to znamená že to nefunguje :D
21:21 mornfall (proto se to ve starších verzích nejmenuje 11, 14, etc... protože není)
21:22 xstill tak třeba relatex constexpr nebudou ani v příštím gcc (což asi bude už 5)
21:22 xstill a 4.7 už mělo c++11 a spoustu nedodělávek k tomu
21:22 xstill takže minimálně u gcc je to takové nejisté
21:22 xstill clang naopak umí skoro celé 14 v 3.4
21:22 mornfall tak jasně, ale ta implikace že pokud to je 1x/1y/1z tak to nefunguje docela sedí
21:22 xstill (prý)
21:23 xstill jo to celkem jo
21:24 xstill až na ten clang 3.4 teda, ten c++14 taky nezná a přitom ho celkem dává
21:45 spito mornfall: hydra nebuildí schválně, nebo omylem?
21:46 mornfall řékl bych že omylem
21:46 mornfall řekl*
22:45 mornfall hydra-evaluator se zasekl, zase jednou
22:45 mornfall je to krize
22:48 xstill zatracený ghci neumí vyhodnotit x <- y pro jiné monády než IO
22:49 mornfall a pak že IO není magický :-))
22:49 xstill samozřejmě že je, to že je to monáda vůbec nevysvětluje, že funguje
22:51 mornfall znám lidi co by řekli že nefunguje
22:52 xstill hm, no, nevím třeba od něj očekávaj jiný věci, ale nevím teda co
22:53 mornfall myVar = unsafePerformIO $ newIORef undefined
22:55 xstill nojo, tak unsafePerformIO je samozřejmě divný
22:56 xstill ale i tak bych očekával že to spadne při pokusu o čtení toho iorefu, což se mi v interpretru neděje
22:56 xstill aha
22:57 xstill ale  let myval = unsafePerformIO $ newIORef (undefined :: Int) in readIORef myval už padá
22:57 xstill takže za to může jen ghci zase
22:58 mornfall > let coerce x = unsafePerformIO (writeIORef myVar x >> readIORef myVar)
22:58 mornfall > coerce (3 :: Int) :: Float
22:58 mornfall 4.0e-45
22:59 xstill wtf
23:00 xstill hej to vůbec nedává typově smysl
23:00 mornfall dává
23:00 xstill aha dává
23:00 mornfall IORef a
23:00 xstill fuj
23:01 xstill to je možná chyba, že něco takového jde vůbec udělat
23:01 mornfall no, je
23:01 xstill ale zase tomu se asi nedá rozumně zabránit
23:03 xstill tak jsem náhodně zkusil coerce True :: Integer, raději to nedělej má to tendeci žrát spoustu paměti
23:04 mornfall :D
23:05 mornfall ono bez unsafePerformIO to udělat nejde
23:05 xstill a teda já už si taky nabil hubu když jsem si myslel, že můžu jen tak chytat výjimky v unsafePerformIO
23:05 mornfall takže to není „až tak“ zlý
23:05 mornfall nojo
23:05 mornfall unsafeInterleaveIO je taky hodně zlý
23:07 xstill to jsem nikdy neviděl
23:07 mornfall tím se implementuje lazy IO (readFile a spol...)
23:08 mornfall zabalíš IO do čistý hodnoty tak aby se spustilo když se to pokusí vyhodnotit
23:37 xstill hm a to jak ghci odvodí z  getLine >>= print .read že ta hodnota má být typu () je taky dost divná magie, naštěstí se to ale děje jen v interpretru
23:38 spito left #divine
23:38 xstill už se toho Haskellu lekl asi

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