Logs: liberachat/#haskell
| 2021-08-17 11:38:28 | → | oxide joins (~lambda@user/oxide) |
| 2021-08-17 11:38:35 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-08-17 11:39:53 | <jophish> | sorry, actually it was the former I think, whatever exports |
| 2021-08-17 11:39:53 | <jophish> | import qualified SDL.Mixer as Mix |
| 2021-08-17 11:40:01 | <jophish> | for some reason I didn't commit a .cabal file |
| 2021-08-17 11:44:12 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Ping timeout: 245 seconds) |
| 2021-08-17 11:45:02 | → | Obo joins (~roberto@185.76.9.42) |
| 2021-08-17 11:46:13 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-08-17 11:46:14 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Remote host closed the connection) |
| 2021-08-17 11:46:21 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-08-17 11:49:52 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Remote host closed the connection) |
| 2021-08-17 11:50:03 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-08-17 11:50:10 | × | Cajun quits (~Cajun@user/cajun) (Quit: Client closed) |
| 2021-08-17 11:51:14 | × | fhutty14 quits (~fhutty14@c83-252-75-55.bredband.tele2.se) (Quit: Client closed) |
| 2021-08-17 11:53:17 | → | fhutty14 joins (~fhutty14@c83-252-75-55.bredband.tele2.se) |
| 2021-08-17 11:53:50 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 3.2) |
| 2021-08-17 11:53:54 | <tomsmeding> | chisui: playing (possibly generated) sound over a speaker, or reading/writing sound files? |
| 2021-08-17 11:54:30 | <chisui> | tomsmeding: playing generated sound over a speaker. |
| 2021-08-17 11:54:47 | <tomsmeding> | then what jophish said :) |
| 2021-08-17 11:54:54 | <tomsmeding> | (otherwise probably https://hackage.haskell.org/package/hsndfile ) |
| 2021-08-17 11:55:19 | → | gambpang joins (~ian@207.181.230.156) |
| 2021-08-17 11:55:45 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 248 seconds) |
| 2021-08-17 11:59:55 | × | gambpang quits (~ian@207.181.230.156) (Ping timeout: 258 seconds) |
| 2021-08-17 12:00:11 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-17 12:00:19 | → | gambpang joins (~ian@207.181.230.156) |
| 2021-08-17 12:03:22 | × | ubert quits (~Thunderbi@91.141.62.226.wireless.dyn.drei.com) (Ping timeout: 258 seconds) |
| 2021-08-17 12:03:23 | ubert1 | is now known as ubert |
| 2021-08-17 12:04:40 | × | mr-red quits (~drd@2001:b07:a70:9f1f:1562:34de:f50f:77d4) (Ping timeout: 240 seconds) |
| 2021-08-17 12:10:01 | × | fhutty14 quits (~fhutty14@c83-252-75-55.bredband.tele2.se) (Quit: Client closed) |
| 2021-08-17 12:10:38 | <chisui> | thanks |
| 2021-08-17 12:11:18 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 12:12:18 | → | ub joins (~Thunderbi@91.141.62.226.wireless.dyn.drei.com) |
| 2021-08-17 12:15:45 | → | Guest65 joins (~Guest65@ppp089210060185.access.hol.gr) |
| 2021-08-17 12:16:03 | × | Guest65 quits (~Guest65@ppp089210060185.access.hol.gr) (Client Quit) |
| 2021-08-17 12:16:40 | × | ub quits (~Thunderbi@91.141.62.226.wireless.dyn.drei.com) (Ping timeout: 240 seconds) |
| 2021-08-17 12:18:19 | × | benin036932 quits (~benin@106.198.88.152) (Ping timeout: 258 seconds) |
| 2021-08-17 12:20:10 | × | xff0x quits (~xff0x@2001:1a81:535d:2700:c2ae:145d:39da:4349) (Ping timeout: 240 seconds) |
| 2021-08-17 12:21:07 | → | xff0x joins (~xff0x@2001:1a81:535d:2700:6b08:445c:db9b:4d20) |
| 2021-08-17 12:22:33 | → | glassy joins (~glassy@90.254.122.50) |
| 2021-08-17 12:22:38 | → | ub joins (~Thunderbi@91.141.62.226.wireless.dyn.drei.com) |
| 2021-08-17 12:23:30 | × | glassy quits (~glassy@90.254.122.50) (Changing host) |
| 2021-08-17 12:23:30 | → | glassy joins (~glassy@user/glassy) |
| 2021-08-17 12:23:32 | → | benin036932 joins (~benin@106.198.88.152) |
| 2021-08-17 12:27:53 | × | trcc quits (~trcc@users-1190.st.net.au.dk) () |
| 2021-08-17 12:30:03 | × | gambpang quits (~ian@207.181.230.156) (Ping timeout: 268 seconds) |
| 2021-08-17 12:30:27 | → | gambpang joins (~ian@207.181.230.156) |
| 2021-08-17 12:32:26 | → | fhutty14 joins (~fhutty14@c83-252-75-55.bredband.tele2.se) |
| 2021-08-17 12:33:08 | × | fhutty14 quits (~fhutty14@c83-252-75-55.bredband.tele2.se) (Client Quit) |
| 2021-08-17 12:34:11 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2021-08-17 12:34:18 | → | notzmv joins (~zmv@user/notzmv) |
| 2021-08-17 12:38:57 | × | sleblanc quits (~sleblanc@user/sleblanc) (Ping timeout: 248 seconds) |
| 2021-08-17 12:39:33 | → | lavaman joins (~lavaman@98.38.249.169) |
| 2021-08-17 12:42:41 | × | benin036932 quits (~benin@106.198.88.152) (Ping timeout: 248 seconds) |
| 2021-08-17 12:43:35 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-17 12:44:40 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 240 seconds) |
| 2021-08-17 12:46:02 | → | benin036932 joins (~benin@106.198.88.152) |
| 2021-08-17 12:46:21 | × | Lycurgus quits (~juan@cpe-45-46-140-49.buffalo.res.rr.com) (Quit: Exeunt) |
| 2021-08-17 12:46:58 | → | pbrisbin joins (~patrick@pool-108-16-214-93.phlapa.fios.verizon.net) |
| 2021-08-17 12:47:32 | × | acidjnk_new3 quits (~acidjnk@p5487d90a.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2021-08-17 12:50:10 | → | shriekingnoise joins (~shrieking@186.137.144.80) |
| 2021-08-17 12:51:56 | × | benin036932 quits (~benin@106.198.88.152) (Read error: Connection reset by peer) |
| 2021-08-17 12:52:07 | → | benin036932 joins (~benin@106.198.88.152) |
| 2021-08-17 12:54:40 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 2021-08-17 12:56:10 | × | raehik1 quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 2021-08-17 12:57:29 | × | benin036932 quits (~benin@106.198.88.152) (Quit: Ping timeout (120 seconds)) |
| 2021-08-17 12:57:50 | → | benin036932 joins (~benin@106.198.88.152) |
| 2021-08-17 12:58:53 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Remote host closed the connection) |
| 2021-08-17 12:59:26 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-08-17 13:00:06 | × | gambpang quits (~ian@207.181.230.156) (Ping timeout: 258 seconds) |
| 2021-08-17 13:00:30 | → | gambpang joins (~ian@207.181.230.156) |
| 2021-08-17 13:02:10 | × | xff0x quits (~xff0x@2001:1a81:535d:2700:6b08:445c:db9b:4d20) (Ping timeout: 240 seconds) |
| 2021-08-17 13:03:58 | × | burnsidesLlama quits (~burnsides@dhcp168-025.wadham.ox.ac.uk) (Ping timeout: 268 seconds) |
| 2021-08-17 13:03:58 | × | ub quits (~Thunderbi@91.141.62.226.wireless.dyn.drei.com) (Ping timeout: 268 seconds) |
| 2021-08-17 13:04:42 | × | ubert quits (~Thunderbi@91.141.62.226.wireless.dyn.drei.com) (Ping timeout: 258 seconds) |
| 2021-08-17 13:05:29 | → | chris joins (~chris@81.96.113.213) |
| 2021-08-17 13:05:33 | chris | is now known as Guest320 |
| 2021-08-17 13:07:02 | × | benin036932 quits (~benin@106.198.88.152) (Ping timeout: 268 seconds) |
| 2021-08-17 13:12:52 | → | xff0x joins (~xff0x@2001:1a81:535d:2700:6b08:445c:db9b:4d20) |
| 2021-08-17 13:13:09 | → | mousey joins (~skymouse@gateway/tor-sasl/mousey) |
| 2021-08-17 13:13:47 | → | benin036932 joins (~benin@106.198.88.152) |
| 2021-08-17 13:17:16 | → | ubert joins (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) |
| 2021-08-17 13:18:08 | <__monty__> | kuribas: Don't expect too much from automated proofs. Afaik Coq is the most advanced constructive logic-based proof assistant in this regard. Proof automation is a lot more useful in the SMT sense. |
| 2021-08-17 13:20:52 | × | dschrempf quits (~dominik@2a01-036d-0118-a2d1-e318-72ef-8701-cb8b.pool6.digikabel.hu) (Quit: WeeChat 3.2) |
| 2021-08-17 13:23:38 | × | ubert quits (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-08-17 13:26:16 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 2021-08-17 13:27:22 | → | burnsidesLlama joins (~burnsides@client-8-71.eduroam.oxuni.org.uk) |
| 2021-08-17 13:29:03 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 244 seconds) |
| 2021-08-17 13:29:24 | <kuribas> | __monty__: can't these use SMT solvers? |
| 2021-08-17 13:29:35 | <kuribas> | I remember there was one for Coq |
| 2021-08-17 13:30:08 | × | notzmv quits (~zmv@user/notzmv) (Read error: Connection reset by peer) |
| 2021-08-17 13:31:38 | <__monty__> | No, SMT solvers are way more limited in what they can do. |
| 2021-08-17 13:31:48 | <__monty__> | Which is why they're amenable to automatic proving : ) |
| 2021-08-17 13:32:25 | <__monty__> | Model checking is much easier than proof search in an enormous search space. |
| 2021-08-17 13:32:26 | → | ubert joins (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) |
| 2021-08-17 13:33:46 | <merijn> | "enormous" is an understatement for "infinite" ;) |
| 2021-08-17 13:34:06 | × | ubert quits (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-08-17 13:34:26 | → | ubert joins (~Thunderbi@91.141.37.36.wireless.dyn.drei.com) |
| 2021-08-17 13:36:03 | <__monty__> | I wasn't sure whether constructive maybe implied countable infinity or even less. So I went with the relatively safe "enormous." |
| 2021-08-17 13:36:05 | × | vgtw quits (~vgtw@c-9164205c.07-348-756d651.bbcust.telenor.se) (Quit: ZNC - https://znc.in) |
| 2021-08-17 13:36:12 | <kuribas> | __monty__: https://smtcoq.github.io/ |
All times are in UTC.