Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 4111 4112 4113 4114 4115 4116 4117 4118 4119 4120 4121 .. 5022
— 502,152 events total
2021-03-29 11:10:15 <ski> bor0 : you might be interested in playing with the Sequent Calculus interactive tutorial, by lexilambda, at <http://logitext.mit.edu/main>
2021-03-29 11:11:00 <ski> er, sorry. wrong person. it's by ezyang (Edward Z. Yang) (sometime in 2012, i think)
2021-03-29 11:12:27 <ski> bor0 : hmm. you want `apply [Go] f P = P', rather than `apply [Go] f P = f P' ?
2021-03-29 11:13:14 <bor0> Thanks for sharing that. I've seen this somewhere. It reminds me of the incredible proof machine https://incredible.pm/
2021-03-29 11:13:25 × star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Excess Flood)
2021-03-29 11:13:46 <ski> it looks like you're using `Go' to terminate the path. i'd just use the end of the list (the empty list), to terminate, so that `apply' knows when to stop descending, and apply the rewriting at the currently reached node
2021-03-29 11:13:49 <bor0> ski, I decided to use GoLeft and GoRight just to traverse and Go to actually Apply. This seems redundant
2021-03-29 11:14:01 <bor0> Heh, we're almost talking the same stuff :D
2021-03-29 11:14:08 × Alleria__ quits (~textual@2603-7000-3040-0000-908d-bfdf-28c9-9e71.res6.spectrum.com) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2021-03-29 11:14:24 × idhugo_ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 246 seconds)
2021-03-29 11:14:43 → star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com)
2021-03-29 11:15:06 <ski> anyway, if applying `f' to a subformula `P' is actually meant to replace it by `f P', rather than leave it untouched (and similarly for `Q',`R'), you could in fact simplify your code, by having a single base case
2021-03-29 11:15:51 → heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5)
2021-03-29 11:16:29 <bor0> How does this look? https://github.com/bor0/misc/commit/84c3bce60f4ce5448aadd561fb08e90d4938a547
2021-03-29 11:16:52 → ddellacosta joins (~ddellacos@86.106.143.196)
2021-03-29 11:16:52 <bor0> Ah. I need to `f P`, `f Q`, `f R`...
2021-03-29 11:17:12 ← jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client")
2021-03-29 11:17:22 × olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Remote host closed the connection)
2021-03-29 11:17:44 ski . o O ( "Go West" by Pet Shop Boys at <https://www.youtube.com/watch?v=LNBjMRvOB5M>,<https://www.youtube.com/watch?v=cfGTm_viXPs> )
2021-03-29 11:17:58 <bor0> Ah, you mean `apply [] f x = f x` would be the base case?
2021-03-29 11:18:13 <ski> yes
2021-03-29 11:19:44 <bor0> OK, I think I finally got it. The rule I shared earlier https://imgur.com/a/l8oV8p0 is basically `eg4` https://github.com/bor0/misc/blob/master/2021/Gentzen.hs#L115 which evaluates to `Or P (Not P)`. Quite satisfying :D
2021-03-29 11:20:22 <ski> and then you don't need the default case at the end (and then you'll get better diagnostics if you change the data type, while using `-Wincomplete-patterns'. cf. `-Wincomplete-uni-patterns',`-Wincomplete-record-updates')
2021-03-29 11:21:02 × Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds)
2021-03-29 11:21:11 <raehik> I'm getting an HTTP 500 when trying to upload a package candidate to Hackage - is there someone I could notify?
2021-03-29 11:21:29 → jakalx joins (~jakalx@base.jakalx.net)
2021-03-29 11:21:46 × ddellacosta quits (~ddellacos@86.106.143.196) (Ping timeout: 268 seconds)
2021-03-29 11:22:10 <merijn> raehik: Is this your first upload?
2021-03-29 11:22:39 → idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net)
2021-03-29 11:22:41 <raehik> merijn: it's the first upload of the package in question, but no I've pushed pkgs before
2021-03-29 11:23:05 <merijn> ah, just checking if maybe you weren't in the uploaders group yet :)
2021-03-29 11:23:40 <raehik> the error says "no space left on resource", seems like /tmp got filled, unsure if it's been caught yet
2021-03-29 11:23:55 <merijn> raehik: There's the #hackage channel and https://github.com/haskell/hackage-server/issues
2021-03-29 11:23:58 <merijn> a
2021-03-29 11:24:26 <merijn> raehik: Hackage mainpage says: "Serious issues requiring immediate action should be reported to admin@haskell.org or on the #haskell-infrastructure irc channel on freenode."
2021-03-29 11:24:31 × heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 245 seconds)
2021-03-29 11:24:41 → idhugo__ joins (~idhugo@87-49-45-185-mobile.dk.customer.tdc.net)
2021-03-29 11:24:43 × Dykam quits (Dykam@dykam.nl) (Quit: Dykam)
2021-03-29 11:24:43 <raehik> merijn: Fab, thanks very much!
2021-03-29 11:26:29 → Dykam joins (Dykam@dykam.nl)
2021-03-29 11:26:58 × idhugo_ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 240 seconds)
2021-03-29 11:29:50 × raichoo quits (~raichoo@dslb-188-109-062-207.188.109.pools.vodafone-ip.de) (Quit: Lost terminal)
2021-03-29 11:32:57 <ph88> does anyone know if hunit has some facilities for test setup and teardown ?
2021-03-29 11:33:03 <ph88> tasty-hunit in particular
2021-03-29 11:36:34 × LKoen quits (~LKoen@65.250.88.92.rev.sfr.net) (Read error: Connection reset by peer)
2021-03-29 11:38:20 → LKoen joins (~LKoen@65.250.88.92.rev.sfr.net)
2021-03-29 11:40:21 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 240 seconds)
2021-03-29 11:41:28 → heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5)
2021-03-29 11:41:46 → ph88^ joins (~ph88@ip5f5af71a.dynamic.kabel-deutschland.de)
2021-03-29 11:42:44 → sord937 joins (~sord937@gateway/tor-sasl/sord937)
2021-03-29 11:43:18 → machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca)
2021-03-29 11:43:43 → Alleria joins (~textual@mskresolve-a.mskcc.org)
2021-03-29 11:44:06 Alleria is now known as Guest23256
2021-03-29 11:45:12 × ph88 quits (~ph88@2a02:8109:9e00:7e5c:e93f:8176:4aa5:ca0b) (Ping timeout: 246 seconds)
2021-03-29 11:46:02 × heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 258 seconds)
2021-03-29 11:48:51 × ixlun quits (~matthew@109.249.184.133) (Read error: Connection reset by peer)
2021-03-29 11:50:12 <dexterfoo> anyone use co-log? How do I use usingLoggerT with fmtRichMessageDefault? The types don't match up
2021-03-29 11:50:19 → geowiesnot joins (~user@87-89-181-157.abo.bbox.fr)
2021-03-29 11:52:29 × flound1129 quits (~flound112@139.28.218.148) (Remote host closed the connection)
2021-03-29 11:54:14 × bor0 quits (~boro@unaffiliated/boro/x-000000001) (Quit: Leaving)
2021-03-29 11:55:48 × acidjnk_new quits (~acidjnk@p200300d0c72b95797030ab852a1672b2.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2021-03-29 11:56:31 × plutoniix quits (~q@184.82.195.122) (Quit: Leaving)
2021-03-29 11:56:51 → ddellacosta joins (~ddellacos@86.106.143.66)
2021-03-29 11:58:08 <xerox_> is there a way to collapse all collapsable dropdowns in an haddock page?
2021-03-29 11:58:30 × Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 246 seconds)
2021-03-29 11:58:56 → acidjnk_new joins (~acidjnk@p200300d0c72b9579218a2a0630d85b14.dip0.t-ipconnect.de)
2021-03-29 12:01:51 × ddellacosta quits (~ddellacos@86.106.143.66) (Ping timeout: 268 seconds)
2021-03-29 12:04:16 × MarcelineVQ quits (~anja@198.254.208.159) (Read error: Connection reset by peer)
2021-03-29 12:07:50 → geekosaur joins (82650c7a@130.101.12.122)
2021-03-29 12:11:32 → csadilek joins (~csadilek@178.239.168.171)
2021-03-29 12:12:09 → __minoru__shirae joins (~shiraeesh@109.166.57.99)
2021-03-29 12:15:29 × coot quits (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl) (Quit: coot)
2021-03-29 12:26:35 → solvr joins (57e3c46d@87.227.196.109)
2021-03-29 12:27:02 → Deide joins (~Deide@217.155.19.23)
2021-03-29 12:27:28 → coot joins (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl)
2021-03-29 12:28:46 → DTZUZU joins (~DTZUZO@205.ip-149-56-132.net)
2021-03-29 12:31:24 × DTZUZU_ quits (~DTZUZO@207.81.119.43) (Ping timeout: 246 seconds)
2021-03-29 12:31:50 → NGravity joins (csp@gateway/shell/xshellz/x-beigeckolcvbhubi)
2021-03-29 12:31:51 × seveg quits (~gabriel@2a02-ab04-0249-8d00-dea6-32ff-fe17-0993.dynamic.v6.chello.sk) (Ping timeout: 252 seconds)
2021-03-29 12:32:22 × geekosaur quits (82650c7a@130.101.12.122) (Ping timeout: 240 seconds)
2021-03-29 12:33:11 → seveg joins (~gabriel@2a02-ab04-0249-8d00-dea6-32ff-fe17-0993.dynamic.v6.chello.sk)
2021-03-29 12:36:35 → urodna joins (~urodna@unaffiliated/urodna)
2021-03-29 12:37:16 → ddellacosta joins (~ddellacos@86.106.143.248)
2021-03-29 12:37:36 × coot quits (~coot@37.30.55.131.nat.umts.dynamic.t-mobile.pl) (Quit: coot)
2021-03-29 12:37:53 → drbean_ joins (~drbean@TC210-63-209-23.static.apol.com.tw)
2021-03-29 12:38:06 × yaroot quits (~yaroot@138.102.13.160.dy.iij4u.or.jp) (Quit: The Lounge - https://thelounge.chat)
2021-03-29 12:38:10 × ubert quits (~Thunderbi@p200300ecdf25d94cca5b76fffe29f233.dip0.t-ipconnect.de) (Remote host closed the connection)
2021-03-29 12:38:14 → zebrag joins (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr)
2021-03-29 12:38:29 → ubert joins (~Thunderbi@p200300ecdf25d94ce6b318fffe838f33.dip0.t-ipconnect.de)
2021-03-29 12:38:48 → yaroot joins (~yaroot@138.102.13.160.dy.iij4u.or.jp)
2021-03-29 12:40:06 → motersen joins (~motersen@217.160.212.240)
2021-03-29 12:40:34 × raym quits (~ray@115.187.32.14) (Quit: leaving)
2021-03-29 12:41:01 <ph88^> merijn, i tried data-files but the data directory is not being made :/
2021-03-29 12:41:21 × gnumonic quits (~gnumonic@c-73-170-91-210.hsd1.ca.comcast.net) (Ping timeout: 260 seconds)
2021-03-29 12:41:56 × ddellacosta quits (~ddellacos@86.106.143.248) (Ping timeout: 268 seconds)
2021-03-29 12:43:37 × Yumasi quits (~guillaume@2a01:e0a:5cb:4430:dbe9:fd6c:d1a9:4bb5) (Ping timeout: 276 seconds)
2021-03-29 12:44:52 → Yumasi joins (~guillaume@static-176-175-104-214.ftth.abo.bbox.fr)
2021-03-29 12:45:24 → geekosaur joins (82650c7a@130.101.12.122)
2021-03-29 12:48:40 × motersen quits (~motersen@217.160.212.240) (Quit: ZNC 1.7.2+deb3 - https://znc.in)
2021-03-29 12:48:53 → motersen joins (~user@2a0a-a540-7dde-0-2d1c-e683-f179-e2a.ipv6dyn.netcologne.de)
←Prev  Next→
Page 1 .. 4111 4112 4113 4114 4115 4116 4117 4118 4119 4120 4121 .. 5022

All times are in UTC.