SHARE
TWEET

Untitled

a guest Jan 22nd, 2020 123 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. [21.01.2020 16:29:39] <bartosz> Przeczytaj o Klee.
  2. [21.01.2020 16:29:55] <bartosz> Wiesz już, co to znaczy "model checking"?
  3. [21.01.2020 16:30:02] <bartosz> Albo "full model construction"?
  4. [21.01.2020 16:31:25] <juliusz.t@haael.com.pl> Model Checking?
  5. [21.01.2020 16:31:38] <bartosz> Wiesz, co to oznacza?
  6. [21.01.2020 16:31:59] <juliusz.t@haael.com.pl> Polega na stworzeniu wiernego modelu układu.
  7. [21.01.2020 16:32:11] <bartosz> Polega na sprawdzeniu wszystkich wartości po kolei.
  8. [21.01.2020 16:32:23] <juliusz.t@haael.com.pl> No, nie zawsze, ale tak.
  9. [21.01.2020 16:32:44] <bartosz> Polega na udowodnieniu kwantyfikatora "dla każdego x" przez fizyczne wykonanie kodu dla każdego x.
  10. [21.01.2020 16:32:48] <bartosz> To jest model checking.
  11. [21.01.2020 16:33:02] <bartosz> Ma złożoność taką, jak rozmiar dziedziny.
  12. [21.01.2020 16:33:11] <bartosz> Jest lepsza metoda.
  13. [21.01.2020 16:33:15] <bartosz> Którą my użyjemy.
  14. [21.01.2020 16:33:25] <bartosz> Jest ona wykorzystywana w klee.
  15. [21.01.2020 16:33:32] <bartosz> Przeczytaj dokładnie, czym jest klee.
  16. [21.01.2020 16:33:36] <bartosz> I naucz tego Maćka.
  17. [21.01.2020 16:36:29] <juliusz.t@haael.com.pl> Okej.
  18. [21.01.2020 16:37:01] <juliusz.t@haael.com.pl> (BTW Jabber dalej nie ma dobrych klientów. PSI kraszuje mi się na Windowsie i muszę restartować cały system.)
  19. [21.01.2020 16:37:51] <bartosz> To raczej problem z Windowsem niż Psi a tym bardziej z Jabberem.
  20. [21.01.2020 16:38:57] <juliusz.t@haael.com.pl> To problem Jabbera, że nie ma dobrych komunikatorów
  21. [21.01.2020 16:39:16] <bartosz> Paulina robi tutorial?
  22. [21.01.2020 16:39:26] <bartosz> Potrzebuję trzech rzeczy.
  23. [21.01.2020 16:39:33] <juliusz.t@haael.com.pl> Tłumaczenie? Wczoraj coś robiła.
  24. [21.01.2020 16:39:34] <bartosz> Pluginu, na podstawie tutoriala.
  25. [21.01.2020 16:39:45] <bartosz> Biblioteki do wyświetlania SVG.
  26. [21.01.2020 16:39:52] <bartosz> I samego interfejsu.
  27. [21.01.2020 16:39:56] <bartosz> I mamy komunikator.
  28. [21.01.2020 16:40:12] <juliusz.t@haael.com.pl> Który będzie się wywalał, ale to pewnie przez system. ;)
  29. [21.01.2020 16:40:22] <juliusz.t@haael.com.pl> Albo będzie działać tylko na jednej platformie.
  30. [21.01.2020 16:40:31] <juliusz.t@haael.com.pl> I nie będzie oferować historii rozmów. :P
  31. [21.01.2020 16:40:33] <bartosz> Mamy odpowiednik apek webowych, które można uruchamiać gdziekolwiek.
  32. [21.01.2020 16:40:41] <bartosz> Historii nie.
  33. [21.01.2020 16:40:52] <bartosz> Czy historia jest zapamiętywana na serwerze?
  34. [21.01.2020 16:41:05] <bartosz> To moje coś nie będzie tworzyć żadnych plików na komputerze.
  35. [21.01.2020 16:41:09] <juliusz.t@haael.com.pl> U nas chyba nie.
  36. [21.01.2020 16:41:16] <juliusz.t@haael.com.pl> Nie wiem, czy Ty tego nie wyłączyłeś.
  37. [21.01.2020 16:41:23] <bartosz> Czy XMPP ma opcję zapisywania historii na serwerze?
  38. [21.01.2020 16:41:34] <juliusz.t@haael.com.pl> Jako użytkownik nie chciałbym o tym wiedzieć. :P
  39. [21.01.2020 16:41:42] <bartosz> Lol.
  40. [21.01.2020 16:41:52] <bartosz> W każdym razie chcę klienta bezstanowego.
  41. [21.01.2020 16:42:12] <bartosz> Logujesz się z dowolnego miejsca i zawsze robi to samo, bo nie ma niczego na dysku.
  42. [21.01.2020 16:45:05] <juliusz.t@haael.com.pl> Szkoda, że bezstanowy nie implikuje, że będzie dobry.
  43. [21.01.2020 16:52:36] <bartosz> Dla mnie dobry = minimalny.
  44. [21.01.2020 16:52:44] <bartosz> Im coś ma mniej opcji, tym lepiej.
  45. [21.01.2020 16:53:00] <bartosz> Lepiej mieć jedną opcję dopracowaną w 100%, niż 100 opcji każdą na 1%.
  46. [21.01.2020 16:53:22] <bartosz> Więc będzie miał tylko obsługę tekstu, SVG i XForms.
  47. [21.01.2020 16:53:31] <juliusz.t@haael.com.pl> Einstein kiedyś powiedział: "Powinno to być tak proste, jak to możliwe, ale nie prostsze."
  48. [21.01.2020 16:53:32] <bartosz> Ale z tych trzech rzeczy można zbudować wszystko.
  49. [21.01.2020 16:53:37] <bartosz> Tak.
  50. [21.01.2020 16:53:57] <bartosz> XMPP zamiast HTTP.
  51. [21.01.2020 16:54:00] <juliusz.t@haael.com.pl> Chamie, żeby się komunikować potrzebuję dobrego komunikatora.
  52. [21.01.2020 16:54:02] <bartosz> SVG zamiast HTML.
  53. [21.01.2020 16:54:18] <bartosz> XForms zamiast HTMLowych formularzy i Javascriptu.
  54. [21.01.2020 16:54:23] <juliusz.t@haael.com.pl> Od komunikatora oczekuję, że będę mógł nadawać, obierać i składować wiadomości.
  55. [21.01.2020 16:54:24] <bartosz> Tekst jako fallback.
  56. [21.01.2020 16:54:43] <juliusz.t@haael.com.pl> Dodatkowo, ma być dostępny wszędzie.
  57. [21.01.2020 16:54:49] <bartosz> To już zadanie dla twórcy interfejsu.
  58. [21.01.2020 16:54:51] <juliusz.t@haael.com.pl> Na każdej platformie.
  59. [21.01.2020 16:54:57] <bartosz> Ktoś będzie musiał zbudować interfejs.
  60. [21.01.2020 16:55:02] <bartosz> Designer.
  61. [21.01.2020 16:55:06] <juliusz.t@haael.com.pl> Ja jestem użytkownikiem.
  62. [21.01.2020 16:55:19] <juliusz.t@haael.com.pl> Nie jestem developerem XMPP, tylko użytkownikiem na Boga.
  63. [21.01.2020 16:55:42] <bartosz> Tylko Ci mówię, jaką drogę wybrałem.
  64. [21.01.2020 16:55:46] <bartosz> I uważam, że jest dobra.
  65. [21.01.2020 16:55:47] <juliusz.t@haael.com.pl> Jestem od Ciebie jeszcze warstwę dalej, niż designer.
  66. [21.01.2020 16:56:06] <juliusz.t@haael.com.pl> Szkoda, że ta droga ma służyć do komunikacji, a podążasz nią sam.
  67. [21.01.2020 16:56:07] <bartosz> Tzn. że przyciągnie designerów w takim samym sensie, jak HTML stworzył profesję webmasterów.
  68. [21.01.2020 16:56:16] <juliusz.t@haael.com.pl> Zatraciłeś gdzieś cel w tej podróży. ;)
  69. [21.01.2020 16:56:34] <juliusz.t@haael.com.pl> Właśnie się przyznałeś.
  70. [21.01.2020 16:56:42] <juliusz.t@haael.com.pl> Nie używasz XMPP do komunikacji.
  71. [21.01.2020 16:56:46] <juliusz.t@haael.com.pl> Masz inny cel.
  72. [21.01.2020 16:57:17] <juliusz.t@haael.com.pl> Twój klient będzie realizował inne cele, niż zapewnienie komunikacji między ludzmi.
  73. [21.01.2020 16:58:09] <juliusz.t@haael.com.pl> Więc proponuję Ci przerzucenie się na coś innego, np. Skype, Messengera lub cokolwiek, co faktycznie służy komunikacji i niczemu więcej. :P
  74. [21.01.2020 16:58:37] <bartosz> :)
  75. [21.01.2020 16:59:07] <bartosz> HTTP też służy do komunikacji a zbudowali na nim znacznie więcej.
  76. [21.01.2020 17:00:41] <juliusz.t@haael.com.pl> "Powinno to być tak proste, jak to możliwe, ale nie prostsze."
  77. [21.01.2020 17:01:00] <juliusz.t@haael.com.pl> HTTP nie służy do komunikacji.
  78. [21.01.2020 17:01:00] <bartosz> :)
  79. [21.01.2020 17:01:08] <juliusz.t@haael.com.pl> Służy do transferu plików.
  80. [21.01.2020 17:01:58] <bartosz> Do transferu plików służy BitTorrent.
  81. [21.01.2020 17:02:37] <juliusz.t@haael.com.pl> HTTP (ang. Hypertext Transfer Protocol) – protokół przesyłania dokumentów hipertekstowych.
  82. [21.01.2020 17:02:44] <juliusz.t@haael.com.pl> Przesyła dokumenty.
  83. [21.01.2020 17:02:54] <juliusz.t@haael.com.pl> Przesyłanie to nie jest komunikacja.
  84. [21.01.2020 17:03:30] <bartosz> A WebRTC?
  85. [21.01.2020 17:04:20] <juliusz.t@haael.com.pl> WebRTC (Web Real-Time Communication) is a free, open-source project that provides web browsers and mobile applications with real-time communication (RTC) via simple application programming interfaces (APIs). It allows audio and video communication to work inside web pages by allowing direct peer-to-peer communication, eliminating the need to install plugins or download native apps.
  86. [21.01.2020 17:05:05] <bartosz> To jest komunikacja za pomocą HTTP między klientami.
  87. [21.01.2020 17:05:39] <juliusz.t@haael.com.pl> Komunikacja to proces nadawania i odbierania wiadomości.
  88. [21.01.2020 17:05:47] <juliusz.t@haael.com.pl> Od komunikatora oczekuje, że mi z tym pomoże.
  89. [21.01.2020 17:05:55] <juliusz.t@haael.com.pl> Jabber nie ma dobrych komunikatorów.
  90. [21.01.2020 17:06:10] <bartosz> Nie ma dobrych interfejsów.
  91. [21.01.2020 17:06:17] <bartosz> Ktoś musi stworzyć interfejs.
  92. [21.01.2020 17:06:26] <juliusz.t@haael.com.pl> A raczej - są inne klienty, które zapewniają komunikację na wyższym poziomie.
  93. [21.01.2020 17:06:34] <juliusz.t@haael.com.pl> Nie interesuje mnie co mają w środku.
  94. [21.01.2020 17:06:41] <juliusz.t@haael.com.pl> Jestem użytkownikiem, a nie developerem.
  95. [21.01.2020 17:06:57] <juliusz.t@haael.com.pl> Nie chcę sobie stworzyć interfejsu, tylko dostać gotowy produkt.
  96. [21.01.2020 17:08:56] <bartosz> Co raz zobaczyłeś, tego nie da się już odzobaczyć.
  97. [21.01.2020 17:09:06] <bartosz> Już nigdy nie zapomnisz, jak działa Jabber :).
  98. [21.01.2020 18:27:26] <juliusz.t@haael.com.pl> Mam problem z zarządzaniem wiadomościami na liście mailowej.
  99. [21.01.2020 18:27:39] <juliusz.t@haael.com.pl> Które wiadomości na pewno nie są istotne?
  100. [21.01.2020 18:28:00] <juliusz.t@haael.com.pl> Dostaję zgłoszenia o bugach. Czy może się pojawić tam coś, co dotyczy stricte nas?
  101. [21.01.2020 19:34:27] <bartosz> Nie.
  102. [21.01.2020 19:34:36] <bartosz> Tylko my coś takiego wysyłamy :).
  103. [21.01.2020 19:34:40] <bartosz> My robimy dowody.
  104. [21.01.2020 19:34:46] <bartosz> Tamto to są developerzy.
  105. [21.01.2020 19:41:42] <juliusz.t@haael.com.pl> Okej.
  106. [21.01.2020 19:41:57] <juliusz.t@haael.com.pl> Prosili, żebyśmy się przedstawili, ale jeszcze tego nie zrobiłem.
  107. [21.01.2020 19:42:03] <juliusz.t@haael.com.pl> Kiedyś coś tam napiszę.
  108. [21.01.2020 19:42:04] <bartosz> Naucz Maćka o tym podejściu klee.
  109. [21.01.2020 19:42:12] <juliusz.t@haael.com.pl> Właśnie czytam o tym.
  110. [21.01.2020 19:42:17] <juliusz.t@haael.com.pl> Ale używają trudnych słów.
  111. [21.01.2020 19:42:40] <bartosz> Nie obiecywałem, że będzie łatwo to wymówić.
  112. [22.01.2020 11:49:07] <juliusz.t@haael.com.pl> Istnieje już kilkanaście implementacji RISC-V.
  113. [22.01.2020 11:49:12] <juliusz.t@haael.com.pl> Po co robić następną?
  114. [22.01.2020 11:49:21] <bartosz> Bo jest nasza?
  115. [22.01.2020 11:49:28] <bartosz> Poza tym tamte nie mają dowodu, tak?
  116. [22.01.2020 11:49:37] <bartosz> Rozumiesz już działanie klee?
  117. [22.01.2020 11:49:42] <juliusz.t@haael.com.pl> Uczę się właśnie.
  118. [22.01.2020 11:49:47] <juliusz.t@haael.com.pl> Ale generalnie widzę o co chodzi.
  119. [22.01.2020 11:49:55] <bartosz> Wyjaśnij.
  120. [22.01.2020 11:50:06] <juliusz.t@haael.com.pl> Tłumaczy kod do LLVM.
  121. [22.01.2020 11:50:27] <juliusz.t@haael.com.pl> Następnie nie podstawia konkretnych wartości, tylko zmienne, do których przypisane są własności.
  122. [22.01.2020 11:51:35] <juliusz.t@haael.com.pl> I jeśli jest wykonywana operacja, to sprawdza, czy nie jest ona niebezpieczna na ogólnym zbiorze, a nie na wartości (np. czy któraś wartość ze zbioru nie wychodzi poza zakres pamięci).
  123. [22.01.2020 11:51:47] <bartosz> Jaki widzisz związek z tym, co robimy w Pythonie?
  124. [22.01.2020 11:52:06] <bartosz> (A do zmiennych w klee nie są przypisane wartości.)
  125. [22.01.2020 11:52:08] <juliusz.t@haael.com.pl> Możemy zamiast LLVM analizować samego Pythona?
  126. [22.01.2020 11:52:28] <bartosz> Napisałeś moduł do arytmetyki modulo.
  127. [22.01.2020 11:52:38] <bartosz> Oraz klasę tworzącą wyrażenia.
  128. [22.01.2020 11:52:48] <bartosz> Jaki widzisz związek z klee?
  129. [22.01.2020 11:53:15] <bartosz> Gdyby stworzyć dwie zmienne w tej klasie od wyrażeń.
  130. [22.01.2020 11:53:27] <bartosz> Tzn. dwa obiekty będące zmiennymi symbolicznymi.
  131. [22.01.2020 11:53:51] <bartosz> Następnie stworzyć dwa obiekty modulo, gdzie zamiast wartości int dajemy im te zmienne symboliczne.
  132. [22.01.2020 11:53:57] <bartosz> A następnie dodać je do siebie.
  133. [22.01.2020 11:54:03] <bartosz> Tzn. te modulo.
  134. [22.01.2020 11:54:06] <bartosz> Co by powstało?
  135. [22.01.2020 11:54:12] <juliusz.t@haael.com.pl> Będziemy mieli wyrażenie, a nie wartość.
  136. [22.01.2020 11:54:59] <bartosz> Jaki widzisz związek z klee?
  137. [22.01.2020 11:55:46] <juliusz.t@haael.com.pl> Klee też korzysta z wartości.
  138. [22.01.2020 11:55:53] <juliusz.t@haael.com.pl> *z wyrażeń.
  139. [22.01.2020 11:55:56] <bartosz> Ech.
  140. [22.01.2020 11:56:02] <bartosz> No tak. Ale jak działa klee?
  141. [22.01.2020 11:56:12] <bartosz> Co robi klee i co robi nasz system?
  142. [22.01.2020 11:56:14] <bartosz> Jaka jest idea?
  143. [22.01.2020 11:56:29] <bartosz> W ogóle rozumiesz, jaki to ma związek z dowodzeniem?
  144. [22.01.2020 11:57:28] <juliusz.t@haael.com.pl> Nie będę zgadywać. Rozumiem, ale nie wiem jakiej odpowiedzi ode mnie oczekujesz.
  145. [22.01.2020 11:58:02] <juliusz.t@haael.com.pl> Samo to, że mamy wyrażenia pozwala formułować własności działań, jakie wykonujemy.
  146. [22.01.2020 11:58:30] <juliusz.t@haael.com.pl> Dowiedzenie posiadania własności jest równoważne, ze spełnieniem jakichś aksjomatów.
  147. [22.01.2020 11:58:36] <bartosz> Uzasadnij, że klee albo nasz system jest w stanie udowodnić, że dana formuła z funkcją w LLVM / Pythonie jest spełniona dla wszystkich wartości.
  148. [22.01.2020 11:58:52] <bartosz>
  149. def f(x):
  150.  return cośtam
  151.  
  152. [22.01.2020 11:59:12] <bartosz> FORALL(x) valid( f( x ) )
  153. [22.01.2020 11:59:15] <bartosz> Ech.
  154. [22.01.2020 11:59:24] <bartosz> FORALL( x ) valid( f( x ) )
  155. [22.01.2020 11:59:39] <bartosz> Masz jakąś funkcję f, w Pythonie.
  156. [22.01.2020 11:59:43] <bartosz> Analogicznie: w LLVM.
  157. [22.01.2020 12:00:14] <bartosz> Ta funkcja nie ma skutków ubocznych ani pętli nie-stałej wielkości (czyli jest obwodem), poza tym może być dowolna.
  158. [22.01.2020 12:00:39] <bartosz> W szczególności może zawierać konstrukcje imperatywne, może się też odwoływać do innych funkcji spełniających te same warunki.
  159. [22.01.2020 12:00:44] <bartosz> Nie ma rekurencji.
  160. [22.01.2020 12:00:58] <bartosz> Uzasadnij, że nasz system albo klee udowodni tą formułę.
  161. [22.01.2020 12:01:31] <bartosz> valid może być też dowolnym predykatem.
  162. [22.01.2020 12:02:00] <bartosz> Wygląda na to, że nie rozumiesz tego jeszcze do końca.
  163. [22.01.2020 12:02:08] <juliusz.t@haael.com.pl> W poradniku inżyniera była reguła wnioskowania "opuszczenia kwantyfikatora ogólnego".
  164. [22.01.2020 12:02:09] <bartosz> Dokończ ten Twój moduł od wyrażeń.
  165. [22.01.2020 12:02:25] <bartosz> Nie w poradniku inżyniera. Jak działa klee?
  166. [22.01.2020 12:02:32] <bartosz> Dokończ ten moduł od wyrażeń.
  167. [22.01.2020 12:02:47] <bartosz> Stwórz dwie zmienne (reprezentujące pythonowe inty).
  168. [22.01.2020 12:03:03] <bartosz> Stwórz dwa obiekty modulo z tymi zmiennymi w miejsce wartości.
  169. [22.01.2020 12:03:25] <bartosz> x = Expression.var('x')
  170. [22.01.2020 12:03:31] <bartosz> y = Expression.var('y')
  171. [22.01.2020 12:03:37] <bartosz> a = Modulo(x)
  172. [22.01.2020 12:03:40] <bartosz> Ech.
  173. [22.01.2020 12:03:43] <bartosz> a = Modulo( x )
  174. [22.01.2020 12:03:47] <bartosz> b = Modulo( y )
  175. [22.01.2020 12:03:52] <bartosz> Udowodnij:
  176. [22.01.2020 12:04:49] <bartosz> FORALL( x, y ) a + b = b + a
  177. [22.01.2020 12:05:10] <bartosz> FORALL( x, y, z ) (a + b) + c == a + (b + c)
  178. [22.01.2020 12:05:23] <bartosz> FORALL( x ) a + Modulo( 0 ) == a
  179. [22.01.2020 12:05:35] <bartosz> FORALL( x ) a + Modulo( 1 ) != a
  180. [22.01.2020 12:05:47] <bartosz> Aksjomaty arytmetyki modulo.
  181. [22.01.2020 12:05:54] <bartosz> Jest jeszcze jeden aksjomat, ale jest długi.
  182. [22.01.2020 12:06:04] <bartosz> Na razie wystarczy, że udowodnisz jeden, dowolny.
  183. [22.01.2020 12:06:24] <bartosz> A w zasadzie: wytłumacz, w jaki sposób klee / nasz system to udowadnia i dlaczego w ogóle to jest dobry dowód.
  184. [22.01.2020 12:07:15] <bartosz> Czy zgadzasz się, że gdyby w jakiś sposób fizycznie sprawdzić te aksjomaty dla wszystkich kombinacji intów po kolei, to to byłby dobry dowód?
  185. [22.01.2020 12:08:08] <juliusz.t@haael.com.pl> Sprawdzenie wszystkich elementów w teorii skończonej to to samo co sprawdzenie formuły z kwantyfikatorem ogólnym.
  186. [22.01.2020 12:08:20] <bartosz> Nieskończonej też :).
  187. [22.01.2020 12:08:27] <bartosz> Na komputerze się nie da, ale matematycznie można.
  188. [22.01.2020 12:08:44] <bartosz> Teraz pokaż, że klee też udowadnia kwantyfikator ogólny.
  189. [22.01.2020 12:08:57] <bartosz> Ale bez sprawdzania wszystkich wartości.
  190. [22.01.2020 12:09:02] <bartosz> Zazwyczaj.
  191. [22.01.2020 12:09:10] <bartosz> Co innego jest złożonością klee.
  192. [22.01.2020 12:09:33] <bartosz> Klee jest ograniczone innym parametrem, nie rozmiarem dziedziny. Jakim?
  193. [22.01.2020 12:09:42] <bartosz> Co decyduje o czasie działania klee?
  194. [22.01.2020 12:11:01] <juliusz.t@haael.com.pl> Chamie, zle się z Tobą pracuje. Jesteś strasznie agresywny w wpowiedziach.
  195. [22.01.2020 12:11:09] <juliusz.t@haael.com.pl> Doczytam o klee i wtedy wrócę.
  196. [22.01.2020 12:11:13] <bartosz> OK.
  197. [22.01.2020 12:11:19] <juliusz.t@haael.com.pl> Postaram się zrobić to zadanie z modulo.
  198. [22.01.2020 12:11:23] <bartosz> OK.
  199. [22.01.2020 12:13:19] <juliusz.t@haael.com.pl> Moja odpowiedz jest taka, że do dowodu z ogólnym wyrażeniem można wprowadzić kwantyfikator ogólny, tak jak w regułach opuszczenia i wprowadzania kwantyfikatora ogólnego.
  200. [22.01.2020 12:13:30] <juliusz.t@haael.com.pl> Jak będę miał lepszą, to napiszę.
  201. [22.01.2020 12:14:01] <bartosz> Przeczytaj, co robi klee, kiedy napotka ifa.
  202. [22.01.2020 12:14:04] <bartosz> Warunek.
  203. [22.01.2020 12:14:13] <bartosz> Twój moduł też.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Top