Logs on 2024-05-25 (liberachat/#haskell)
| 00:01:27 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Excess Flood) |
| 00:02:07 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 00:02:09 | → | fizbin__ joins (~fizbin@user/fizbin) |
| 00:04:36 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Excess Flood) |
| 00:05:23 | × | Luj quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 00:05:48 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 00:06:07 | → | Luj joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 00:09:51 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 00:12:45 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 00:18:47 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 00:19:02 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 00:21:43 | × | Luj quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 00:22:10 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 00:22:18 | → | Luj joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 00:22:36 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Quit: diagnostics0) |
| 00:23:04 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 00:36:13 | → | TheCoffeMaker_ joins (~TheCoffeM@200.114.213.75) |
| 00:36:29 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Ping timeout: 240 seconds) |
| 00:46:59 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Quit: diagnostics0) |
| 00:51:21 | × | terrorjack quits (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
| 00:54:16 | → | terrorjack joins (~terrorjac@2a01:4f8:c17:87f8::) |
| 01:00:04 | × | TheCoffeMaker_ quits (~TheCoffeM@200.114.213.75) (Read error: Connection reset by peer) |
| 01:00:50 | → | talismanick joins (~user@2601:644:937c:ed10::ae5) |
| 01:01:34 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 01:03:01 | × | CrunchyFlakes quits (~CrunchyFl@146.52.130.128) (Ping timeout: 255 seconds) |
| 01:04:09 | → | CrunchyFlakes joins (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) |
| 01:06:29 | × | Square2 quits (~Square@user/square) (Ping timeout: 240 seconds) |
| 01:24:04 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 01:24:15 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Remote host closed the connection) |
| 01:24:36 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 01:26:05 | × | RedFlamingos quits (~RedFlamin@user/RedFlamingos) (Quit: RedFlamingos) |
| 01:29:23 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Ping timeout: 264 seconds) |
| 01:30:54 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 01:42:28 | × | Midjak quits (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep) |
| 01:53:38 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 01:57:25 | × | otto_s quits (~user@p5de2f772.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 01:58:55 | → | otto_s joins (~user@p5de2f67f.dip0.t-ipconnect.de) |
| 02:00:02 | × | fliife quits (~fliife@user/fliife) (Quit: ZNC 1.8.2+deb2build5 - https://znc.in) |
| 02:00:49 | → | fliife joins (~fliife@user/fliife) |
| 02:07:58 | <cpli> | is there some (define-syntax prepend-a- [...] ) which transforms (prepend-a- proc) into (a-proc)? |
| 02:08:40 | <glguy> | In Haskell? |
| 02:38:40 | × | dolio quits (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in) |
| 02:43:03 | × | troydm quits (~troydm@user/troydm) (Ping timeout: 268 seconds) |
| 02:44:26 | → | dolio joins (~dolio@130.44.134.54) |
| 02:44:47 | × | dolio quits (~dolio@130.44.134.54) (Client Quit) |
| 02:48:09 | → | dolio joins (~dolio@130.44.134.54) |
| 02:52:55 | × | fizbin__ quits (~fizbin@user/fizbin) (Ping timeout: 268 seconds) |
| 02:56:59 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 260 seconds) |
| 02:59:46 | × | td_ quits (~td@i53870918.versanet.de) (Ping timeout: 256 seconds) |
| 03:01:45 | → | td_ joins (~td@i53870937.versanet.de) |
| 03:06:42 | × | dolio quits (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in) |
| 03:14:25 | → | dolio joins (~dolio@130.44.134.54) |
| 03:25:19 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 03:28:40 | → | fizbin__ joins (~fizbin@user/fizbin) |
| 03:31:25 | × | dolio quits (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in) |
| 03:40:37 | → | dolio joins (~dolio@130.44.134.54) |
| 03:46:24 | × | xigua quits (~xigua@user/xigua) (Read error: Connection reset by peer) |
| 03:46:38 | → | xigua joins (~xigua@user/xigua) |
| 03:51:35 | × | dolio quits (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in) |
| 03:53:53 | → | dolio joins (~dolio@130.44.134.54) |
| 04:05:17 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 240 seconds) |
| 04:08:24 | × | dolio quits (~dolio@130.44.134.54) (Quit: ZNC 1.8.2 - https://znc.in) |
| 04:10:41 | → | dolio joins (~dolio@130.44.134.54) |
| 04:21:58 | × | phma quits (~phma@host-67-44-208-17.hnremote.net) (Read error: Connection reset by peer) |
| 04:27:41 | × | fizbin__ quits (~fizbin@user/fizbin) (Ping timeout: 240 seconds) |
| 04:30:12 | → | phma joins (~phma@host-67-44-208-55.hnremote.net) |
| 04:45:07 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 04:53:59 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds) |
| 04:55:41 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:01:20 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 05:15:12 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection) |
| 05:19:22 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:29:23 | → | quark17 joins (~quark17@125-237-181-192-adsl.sparkbb.co.nz) |
| 05:31:07 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection) |
| 05:33:44 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:56:23 | → | oo_miguel joins (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 06:03:41 | × | jle` quits (~jle`@2603:8001:3b02:84d4:f1eb:615d:e4c3:d09c) (Ping timeout: 240 seconds) |
| 06:04:48 | → | jle` joins (~jle`@2603:8001:3b02:84d4:f047:2251:133c:1d1c) |
| 06:17:29 | → | burnsidesLlama joins (~burnsides@119247164140.ctinets.com) |
| 06:17:30 | × | burnsidesLlama quits (~burnsides@119247164140.ctinets.com) (Client Quit) |
| 06:18:14 | × | quark17 quits (~quark17@125-237-181-192-adsl.sparkbb.co.nz) (Quit: Connection closed) |
| 06:20:52 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 06:32:29 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 240 seconds) |
| 06:33:49 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 06:42:54 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 06:44:15 | × | oo_miguel quits (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 260 seconds) |
| 06:53:42 | → | euphores joins (~SASL_euph@user/euphores) |
| 06:56:42 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 06:58:11 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 264 seconds) |
| 07:04:11 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 07:04:33 | → | euleritian joins (~euleritia@dynamic-176-006-195-061.176.6.pool.telefonica.de) |
| 07:10:41 | → | troydm joins (~troydm@user/troydm) |
| 07:16:49 | → | rvalue joins (~rvalue@user/rvalue) |
| 07:17:23 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 264 seconds) |
| 07:18:33 | × | jrm quits (~jrm@user/jrm) (Quit: ciao) |
| 07:18:56 | → | jrm joins (~jrm@user/jrm) |
| 07:19:21 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:20:02 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 07:20:56 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 07:21:55 | × | euleritian quits (~euleritia@dynamic-176-006-195-061.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:22:37 | → | euleritian joins (~euleritia@77.22.252.56) |
| 07:24:55 | × | euleritian quits (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
| 07:25:14 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:26:06 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 07:26:31 | → | acidjnk joins (~acidjnk@p200300d6e714dc042020e32aab5643b9.dip0.t-ipconnect.de) |
| 07:27:23 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 07:30:36 | → | poscat joins (~poscat@user/poscat) |
| 07:31:17 | × | Pixi quits (~Pixi@user/pixi) (Ping timeout: 240 seconds) |
| 07:40:40 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 07:51:59 | → | Pixi joins (~Pixi@user/pixi) |
| 07:53:58 | → | titibandit joins (~user@user/titibandit) |
| 07:59:18 | → | __monty__ joins (~toonn@user/toonn) |
| 07:59:18 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 08:00:59 | → | gmg joins (~user@user/gehmehgeh) |
| 08:15:48 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 08:17:14 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 08:17:56 | → | gmg joins (~user@user/gehmehgeh) |
| 08:18:35 | × | Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 264 seconds) |
| 08:21:17 | <tomsmeding> | cpli: there is template haskell, with which you could define a thing so that $(prependA 'proc) becomes a reference to `aProc` |
| 08:22:51 | <tomsmeding> | prependA name = return (VarE (mkName ("a" ++ nameBase name))) -- using `import Language.Haskell.TH` from "template-haskell" |
| 08:22:55 | → | Maxdamantus joins (~Maxdamant@user/maxdamantus) |
| 08:23:05 | <tomsmeding> | of course that doesn't capitalise the 'P' but that's an exercise to the reader :) |
| 08:33:35 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 08:34:14 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 08:35:47 | <ski> | (`define-syntax' is Scheme, fwiw) |
| 08:54:14 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 09:06:12 | → | euleritian joins (~euleritia@77.22.252.56) |
| 09:07:14 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 268 seconds) |
| 09:08:46 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 09:10:52 | → | mreh joins (~matthew@host86-160-168-107.range86-160.btcentralplus.com) |
| 09:13:01 | <mreh> | I was looking for a canonical example of concurrent haskell and I've just tried running the `Synchronisation with locks` example in here https://wiki.haskell.org/Haskell_for_multicores but I don't see any speedup at all. In fact it's slower for me. |
| 09:13:43 | <sm> | sounds about right :) |
| 09:14:25 | <mreh> | It's also slower than if I run it single threaded and fork subshells to run it. |
| 09:15:14 | <Rembane> | mreh: Can you show us your code? |
| 09:15:43 | <mreh> | Rembane: it's there under the heading `Synchronisation with locks`. |
| 09:15:49 | <mreh> | I've just cut and paste |
| 09:16:11 | <Rembane> | mreh: Thank you! |
| 09:16:36 | <mreh> | I dumped it into a stack project. Maybe I need to look and see what compile flags precisely stack is using.. |
| 09:17:48 | <mreh> | I've got `-threaded -rtsopts -with-rtsopts=-N` in my package.yaml for the executable. |
| 09:18:33 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 09:18:36 | <mreh> | CPU utilisation goes up to X00% where X is roughly equal to the number of threads spawned (= to the number of arguments passed) |
| 09:19:06 | <mreh> | GC time in the output of `+RTS -s` is practically nothing. |
| 09:21:31 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 09:22:03 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 09:25:22 | <mreh> | Okay, I just tried again and removed a modification I forgot I made. I had removed the bang pattern and stuck in h `seq` putMVar str (f ++ ": " ++ h) |
| 09:25:39 | <mreh> | did I need to use `evaluate` there? |
| 09:27:37 | <tomsmeding> | inside IO it's always prudent to use `evaluate` |
| 09:28:12 | <tomsmeding> | mreh: how long is that process running? |
| 09:28:17 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
| 09:28:33 | <tomsmeding> | if it's too short, GHC might not get the opportunity to reschedule the forkIO'd threads to separate cores |
| 09:29:13 | <tomsmeding> | oh you said that cpu utilisation goes up to X00% |
| 09:29:34 | <tomsmeding> | that is odd in combination with the rest |
| 09:30:27 | <mreh> | yeah, which is why I never suspected and strictness problem |
| 09:30:39 | <mreh> | or, laziness problem.. ahem |
| 09:31:08 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:35:29 | → | ACuriousMoose0 joins (~ACuriousM@142.68.181.38) |
| 09:35:33 | × | ACuriousMoose quits (~ACuriousM@142.68.181.38) (Ping timeout: 255 seconds) |
| 09:35:33 | ACuriousMoose0 | is now known as ACuriousMoose |
| 09:38:17 | → | rvalue joins (~rvalue@user/rvalue) |
| 09:45:22 | <mreh> | Okay, so it scales well while I add more than 2 threads, but there's a huge jump in mutator time between +RTS -N1 and +RTS -N2 |
| 09:45:37 | <mreh> | It goes from 2s to 6 seconds |
| 09:45:56 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 09:47:45 | <mreh> | This is running the code under `Synchronisation with locks` as it was written on here https://wiki.haskell.org/Haskell_for_multicores |
| 09:55:57 | × | euleritian quits (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
| 09:56:04 | → | euleritian joins (~euleritia@77.22.252.56) |
| 10:08:59 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:13:19 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 10:19:08 | × | euleritian quits (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
| 10:19:47 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 10:26:48 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 10:48:48 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 10:53:03 | → | danza joins (~francesco@151.57.252.139) |
| 10:54:50 | × | danza quits (~francesco@151.57.252.139) (Remote host closed the connection) |
| 10:55:14 | → | danza joins (~francesco@151.57.252.139) |
| 10:57:56 | × | mreh quits (~matthew@host86-160-168-107.range86-160.btcentralplus.com) (Ping timeout: 252 seconds) |
| 11:07:00 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 11:07:41 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 11:08:47 | × | danza quits (~francesco@151.57.252.139) (Remote host closed the connection) |
| 11:08:54 | → | danza joins (~francesco@151.57.252.139) |
| 11:12:05 | × | justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 240 seconds) |
| 11:14:21 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 11:16:55 | × | patrl quits (~patrl@user/patrl) (Read error: Connection reset by peer) |
| 11:17:09 | → | patrl joins (~patrl@user/patrl) |
| 11:21:27 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 11:21:27 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 11:21:34 | → | euleritian joins (~euleritia@dynamic-176-006-195-061.176.6.pool.telefonica.de) |
| 11:41:03 | × | acidjnk quits (~acidjnk@p200300d6e714dc042020e32aab5643b9.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 11:41:12 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 11:41:23 | → | Square2 joins (~Square@user/square) |
| 11:41:26 | → | Midjak joins (~MarciZ@82.66.147.146) |
| 11:43:26 | × | Midjak quits (~MarciZ@82.66.147.146) (Remote host closed the connection) |
| 11:44:59 | → | tremon joins (~tremon@83.80.159.219) |
| 12:08:30 | → | zetef joins (~quassel@5.14.129.80) |
| 12:17:10 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 12:30:30 | × | mei quits (~mei@user/mei) (Quit: mei) |
| 12:32:05 | → | mei joins (~mei@user/mei) |
| 12:43:06 | × | Luj quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 12:43:41 | → | Luj joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 12:46:52 | × | Luj quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Client Quit) |
| 12:47:31 | → | Luj joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 12:50:02 | → | acidjnk joins (~acidjnk@p200300d6e714dc042020e32aab5643b9.dip0.t-ipconnect.de) |
| 13:02:27 | × | causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.1.1) |
| 13:12:16 | × | Square2 quits (~Square@user/square) (Ping timeout: 260 seconds) |
| 13:33:05 | × | Luj quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 13:33:41 | → | Luj joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 14:07:39 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 14:08:30 | × | zetef quits (~quassel@5.14.129.80) (Remote host closed the connection) |
| 14:10:02 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 14:12:15 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 14:18:43 | → | danza_ joins (~francesco@151.37.228.150) |
| 14:21:17 | × | danza quits (~francesco@151.57.252.139) (Read error: Connection reset by peer) |
| 14:25:07 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 14:31:39 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 14:44:23 | × | AlexZenon quits (~alzenon@5.139.233.209) (Read error: Connection reset by peer) |
| 14:44:45 | → | AlexZenon joins (~alzenon@5.139.233.209) |
| 14:52:40 | → | billchenchina joins (~billchenc@103.152.35.21) |
| 14:53:45 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 14:56:00 | × | euleritian quits (~euleritia@dynamic-176-006-195-061.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 14:56:17 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 14:57:08 | → | edrx joins (~Eduardo@179-191-223-123.static.sumicity.net.br) |
| 14:58:44 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Ping timeout: 268 seconds) |
| 14:59:35 | <edrx> | hi all! I am a basic user of both Haskell and Lean4, and this question originated on Lean, but I would like to know how it can be handled in Haskell too... |
| 14:59:36 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:01:34 | <edrx> | Lean4 has lots of tools for metaprogramming - for example, we can put that in a line a lean program |
| 15:01:40 | <edrx> | run_cmd Lean.logInfo (← Lean.getCurrNamespace) |
| 15:03:45 | <edrx> | and run_cmd will have access to the monads that hold the parsers, the current definitions, etc - and that line will print the current namespace at that point in the window with the logs, warnings, and errors. |
| 15:04:38 | <edrx> | I was trying to use run_cmd to inspect these data structures but they have many fields and many classes |
| 15:04:50 | → | cawfee joins (~root@2406:3003:2077:1c50::babe) |
| 15:05:21 | × | cawfee quits (~root@2406:3003:2077:1c50::babe) (Client Quit) |
| 15:05:31 | → | cawfee joins (~root@2406:3003:2077:1c50::babe) |
| 15:05:42 | × | cawfee quits (~root@2406:3003:2077:1c50::babe) (Client Quit) |
| 15:05:51 | → | cawfee joins (~root@2406:3003:2077:1c50::babe) |
| 15:06:32 | <edrx> | now the question - that applies to both Lean and Haskell |
| 15:07:22 | <edrx> | suppose that I am trying to debug a program, and I need to inspect an object at a certain point. |
| 15:09:56 | <edrx> | that object has "fields", "subfields", and "subsubfields" - at that point that object, that is ot type Syntax, is of the form "node info kind args", where the constructor "node" is this one... |
| 15:12:15 | <edrx> | oops, sorry - here are links to the definition of the type Syntax and to its constructor node: |
| 15:12:20 | <edrx> | https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L3685 |
| 15:12:20 | <edrx> | https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L3708 |
| 15:13:18 | <edrx> | and I want to inspect the "info" field, that it of type SourceInfo |
| 15:14:18 | <edrx> | and that field is of the form "original leading pos trailing endPos" |
| 15:14:46 | <edrx> | and I want to inspect its field "leading", that is of type Substring |
| 15:14:54 | <edrx> | etc etc |
| 15:16:47 | <edrx> | I do these things a lot in the languages that I use most, that are Lua and Emacs Lisp... but in Haskell and Lean I don't have any idea of how to that in a way that is not very clumsy - like a series of lets and ifs in a do block |
| 15:17:57 | <edrx> | any suggestion? I mean, besides "this is exactly the wrong way of debugging in Haskell"? |
| 15:20:07 | × | danza_ quits (~francesco@151.37.228.150) (Read error: Connection reset by peer) |
| 15:37:54 | → | bjorkintosh joins (~bjork@user/bjorkintosh) |
| 15:42:26 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 15:44:25 | × | Luj quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 15:45:02 | → | Luj joins (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 15:54:24 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 16:00:43 | × | tremon quits (~tremon@83.80.159.219) (Remote host closed the connection) |
| 16:02:38 | → | tremon joins (~tremon@83.80.159.219) |
| 16:10:30 | <mauke> | edrx: is your question how to access a deeply nested field that may not even exist? |
| 16:10:56 | <mauke> | due to the intermediate structures being sum types |
| 16:14:39 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 16:15:07 | <mauke> | if it's just a one-off thing, you can pattern match arbitrarily deep: case x of { Node (Original s _ _ _) _ _ -> Just s; _ -> Nothing } |
| 16:15:29 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 16:15:37 | <mauke> | otherwise I'd probably look at lenses/prisms because they're bound to have some operators for this |
| 16:19:05 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 16:19:06 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 16:22:11 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 264 seconds) |
| 16:32:56 | <edrx> | mauke: yes - formally they may not exist, but I'm in a case in which I know that they exist, so I'd like to reduce the error handling to a mininum... |
| 16:33:57 | <edrx> | mauke: about "case x of { Node (Original s _ _ _) _ _ -> Just s; _ -> Nothing }" - thanks, I had not written the code yet! |
| 16:35:50 | <mauke> | you can also use a pattern on the LHS of a let binding, but if it doesn't actually match at runtime, it'll error |
| 16:36:16 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 16:36:31 | <edrx> | mauke: in Lean it should be possible to write macros for that, but that's above my skills ATM, so I need to start doing everything by hand |
| 16:37:23 | <edrx> | mauke: so the let acts as a "case" thing with two cases, and the second - that yield an error - is implicit? |
| 16:38:03 | <mauke> | pretty much, but IIRC it's lazy |
| 16:38:12 | <edrx> | mauke: if you have an example of that that will help me a lot |
| 16:38:21 | <mauke> | > let (Just x) = Nothing in length [x, x, x] |
| 16:38:22 | <lambdabot> | 3 |
| 16:38:25 | <mauke> | > let (Just x) = Nothing in x |
| 16:38:27 | <lambdabot> | *Exception: <interactive>:3:5-22: Non-exhaustive patterns in Just x |
| 16:38:33 | <edrx> | thanks!!! |
| 16:39:14 | <edrx> | I need to go to a place without internet now but I'll try to digest that =) thanks a lot!!! =) |
| 16:39:20 | ← | edrx parts (~Eduardo@179-191-223-123.static.sumicity.net.br) (Killed buffer) |
| 16:40:12 | <mauke> | heh, IRCing from emacs |
| 16:40:19 | <mauke> | and/or brazil |
| 16:40:50 | → | mreh joins (~matthew@host86-160-168-107.range86-160.btcentralplus.com) |
| 16:42:44 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 260 seconds) |
| 16:53:45 | <ski> | they're an emacser, has advertized some convenience (?) mode in #emacs |
| 16:55:53 | → | gdown joins (~gavin@h69-11-149-109.kndrid.broadband.dynamic.tds.net) |
| 16:56:32 | → | ystael joins (~ystael@user/ystael) |
| 17:03:41 | × | mreh quits (~matthew@host86-160-168-107.range86-160.btcentralplus.com) (Ping timeout: 252 seconds) |
| 17:04:28 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 17:07:48 | × | mud quits (~mud@user/kadoban) (Quit: quit) |
| 17:08:35 | × | troydm quits (~troydm@user/troydm) (Ping timeout: 272 seconds) |
| 17:11:38 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:14:05 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 240 seconds) |
| 17:16:04 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:17:51 | → | Square2 joins (~Square@user/square) |
| 17:24:06 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:31:26 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 18:05:58 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 18:09:26 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:10:06 | × | gdown quits (~gavin@h69-11-149-109.kndrid.broadband.dynamic.tds.net) (Remote host closed the connection) |
| 18:16:50 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 18:17:14 | → | euphores joins (~SASL_euph@user/euphores) |
| 18:19:18 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 18:29:17 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:37:05 | × | tabemann quits (~tabemann@2600:1700:7990:24e0:1adf:6622:dda2:d177) (Remote host closed the connection) |
| 18:37:25 | → | tabemann joins (~tabemann@2600:1700:7990:24e0:ed03:9e52:504:2b59) |
| 18:43:28 | → | raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 18:44:27 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 18:44:49 | → | califax joins (~califax@user/califx) |
| 18:57:23 | × | destituion quits (~destituio@2a02:2121:607:127a:4f91:ebdf:f515:bca9) (Ping timeout: 256 seconds) |
| 18:57:45 | → | destituion joins (~destituio@2001:4644:c37:0:6086:64f4:a213:b80d) |
| 19:18:21 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 19:35:03 | × | billchenchina quits (~billchenc@103.152.35.21) (Remote host closed the connection) |
| 19:36:53 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 20:14:32 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 20:16:04 | → | michalz joins (~michalz@185.246.207.215) |
| 20:18:28 | × | paddymahoney quits (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 256 seconds) |
| 20:22:11 | → | paddymahoney joins (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 20:24:26 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 20:24:41 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Remote host closed the connection) |
| 20:25:02 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 20:25:23 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Read error: Connection reset by peer) |
| 20:25:44 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 20:26:11 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Remote host closed the connection) |
| 20:26:28 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 20:26:49 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Read error: Connection reset by peer) |
| 20:26:58 | × | tremon quits (~tremon@83.80.159.219) (Remote host closed the connection) |
| 20:27:07 | → | diagnostics0 joins (~diagnosti@38.22.211.237) |
| 20:27:58 | × | diagnostics0 quits (~diagnosti@38.22.211.237) (Read error: Connection reset by peer) |
| 20:43:55 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 256 seconds) |
| 20:43:56 | × | Eoco quits (~ian@128.101.131.218) (Quit: WeeChat 4.1.1) |
| 20:50:54 | → | phma_ joins (phma@2001:5b0:2144:1aa8:afa6:899b:a052:d2db) |
| 20:52:42 | × | phma quits (~phma@host-67-44-208-55.hnremote.net) (Read error: Connection reset by peer) |
| 20:58:29 | → | mreh joins (~mreh@2a00:23c7:2803:ef01:d717:6c61:accb:b053) |
| 21:00:14 | × | mreh quits (~mreh@2a00:23c7:2803:ef01:d717:6c61:accb:b053) (Client Quit) |
| 21:10:10 | × | phma_ quits (phma@2001:5b0:2144:1aa8:afa6:899b:a052:d2db) (Read error: Connection reset by peer) |
| 21:10:54 | → | phma_ joins (~phma@host-67-44-208-128.hnremote.net) |
| 21:12:47 | × | lbseale_ quits (~quassel@user/ep1ctetus) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 21:23:37 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:25:21 | → | pavonia joins (~user@user/siracusa) |
| 21:26:13 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:28:35 | × | michalz quits (~michalz@185.246.207.215) (Quit: ZNC 1.9.0 - https://znc.in) |
| 21:29:11 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:31:26 | → | Eoco joins (~ian@128.101.131.218) |
| 21:33:44 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 21:37:45 | × | destituion quits (~destituio@2001:4644:c37:0:6086:64f4:a213:b80d) (Ping timeout: 272 seconds) |
| 21:37:46 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:38:17 | → | destituion joins (~destituio@2a02:2121:607:127a:8ad9:5c0a:45fb:3e09) |
| 21:39:04 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 21:39:35 | → | rvalue joins (~rvalue@user/rvalue) |
| 21:53:59 | × | raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds) |
| 21:56:23 | × | paddymahoney quits (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 264 seconds) |
| 22:03:13 | → | paddymahoney joins (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 22:09:21 | × | misterfish quits (~misterfis@84.53.85.146) (Remote host closed the connection) |
| 22:11:08 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 22:13:41 | → | kadir joins (~kadir@88.251.51.100) |
| 22:15:59 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 22:22:00 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 22:22:40 | → | euleritian joins (~euleritia@dynamic-176-006-185-100.176.6.pool.telefonica.de) |
| 22:25:32 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:29:07 | phma_ | is now known as phma |
| 22:30:45 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 22:34:10 | → | causal joins (~eric@50.35.88.207) |
| 22:34:54 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 22:42:53 | × | titibandit quits (~user@user/titibandit) (Ping timeout: 240 seconds) |
| 22:45:35 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 22:50:01 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 23:06:20 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 23:12:24 | × | acidjnk quits (~acidjnk@p200300d6e714dc042020e32aab5643b9.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 23:12:59 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 23:13:14 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 23:15:35 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 23:17:47 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 23:24:43 | × | kadir quits (~kadir@88.251.51.100) (Quit: WeeChat 4.2.2) |
| 23:26:22 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 23:33:13 | × | hiredman quits (~hiredman@frontier1.downey.family) (Quit: Lost terminal) |
| 23:55:47 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
All times are in UTC on 2024-05-25.