Logs: liberachat/#haskell
| 2026-04-27 19:00:18 | → | redshuffle joins (~quassel@45.43.70.75) |
| 2026-04-27 19:01:56 | layline-away | is now known as layline_ |
| 2026-04-27 19:02:15 | layline_ | is now known as layline-away |
| 2026-04-27 19:03:42 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 19:03:48 | layline-away | is now known as layline_ |
| 2026-04-27 19:04:56 | <__monty__> | Enumerating is pretty much what model checkers do, no? And SMT solvers kinda. |
| 2026-04-27 19:05:29 | × | r1bilski_ quits (~r1bilski@user-31-175-22-58.play-internet.pl) (Ping timeout: 252 seconds) |
| 2026-04-27 19:08:05 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-27 19:08:33 | <int-e> | __monty__: Not really. The point of these tools is generally to work symbolically. But there's usually a lot of case splitting, which adds an enumerative flavor, and can degernate into enumerating all possible cases. |
| 2026-04-27 19:12:36 | <int-e> | Even modern SAT solvers (which operate with boolean variables, so everything is discrete) are primarily trying to find forced inferences that allow better pruning of the search space, and a good order in which to try variables. They restart a lot (wiping the whole search tree)) |
| 2026-04-27 19:13:29 | <int-e> | (but keeping learned clauses and information about how fruitful variables are for finding forced inferences (i.e., pruning the search tree early)) |
| 2026-04-27 19:13:33 | <__monty__> | I didn't say they were exhaustive. But they do "enumerate" through relevant classes of values, no? |
| 2026-04-27 19:14:06 | <int-e> | it's just the least important and interesting aspect of these solvers |
| 2026-04-27 19:14:14 | <int-e> | that's my objection |
| 2026-04-27 19:15:15 | <__monty__> | I may just not be good at using them, causing my observations of their working to skew towards lengthy enumerations : ) |
| 2026-04-27 19:16:29 | <int-e> | __monty__: that's not a contradiction; your search space (from splitting into cases) can explode long before you exhaust all possibilities (which may even be infinite) |
| 2026-04-27 19:17:11 | <int-e> | "enumerate", to me, means covering all possible cases (assignments of variables) |
| 2026-04-27 19:17:14 | → | pavonia joins (~user@user/siracusa) |
| 2026-04-27 19:19:01 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 19:21:56 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2026-04-27 19:23:14 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-27 19:26:24 | × | target_i quits (~target_i@user/target-i/x-6023099) (Ping timeout: 255 seconds) |
| 2026-04-27 19:27:17 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2026-04-27 19:28:51 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Remote host closed the connection) |
| 2026-04-27 19:34:24 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 19:35:04 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 276 seconds) |
| 2026-04-27 19:35:19 | layline_ | is now known as layline-away |
| 2026-04-27 19:36:23 | → | ezzieyguywuf joins (~Unknown@user/ezzieyguywuf) |
| 2026-04-27 19:36:29 | × | Googulator53 quits (~Googulato@78-131-16-66.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-27 19:36:55 | → | Googulator53 joins (~Googulato@78-131-16-66.pool.digikabel.hu) |
| 2026-04-27 19:39:03 | × | layline-away quits (~layline@149.154.26.56) (Quit: ZZZzzz…) |
| 2026-04-27 19:39:44 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-04-27 19:44:57 | <davean> | Yah and SMT solvers very much try to NOT have to cover all of them |
| 2026-04-27 19:45:26 | <davean> | They can be forced into enumeration but they try to avoid it and do only a ... pertial enumeration, not to feed __monty__ |
| 2026-04-27 19:48:05 | → | r1bilski_ joins (~r1bilski@user-31-175-22-58.play-internet.pl) |
| 2026-04-27 19:50:27 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 19:54:32 | × | tromp quits (~textual@2001:1c00:340e:2700:144f:94ac:cf96:df60) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-27 19:55:13 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-27 19:57:13 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 2026-04-27 19:58:30 | × | gabriel_sevecek quits (~gabriel@92-180-224-71.dynamic.orange.sk) (Quit: WeeChat 4.9.0) |
| 2026-04-27 19:59:04 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2026-04-27 19:59:35 | → | gabriel_sevecek joins (~gabriel@92-180-224-71.dynamic.orange.sk) |
| 2026-04-27 19:59:58 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 2026-04-27 20:00:03 | ← | thenightmail` parts (~whoareyou@user/thenightmail) (ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.2)) |
| 2026-04-27 20:00:17 | × | michalz quits (~michalz@185.246.207.203) (Remote host closed the connection) |
| 2026-04-27 20:01:56 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2026-04-27 20:06:01 | × | puke quits (~puke@user/puke) (Read error: Connection reset by peer) |
| 2026-04-27 20:06:11 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 20:06:19 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-04-27 20:11:28 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-04-27 20:12:16 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2026-04-27 20:13:35 | → | __monty__ joins (~toonn@user/toonn) |
| 2026-04-27 20:17:16 | <haskellbridge> | <ijouw> I am trying to use PosixPath but am stuck on how I enumerate things in a directory or convert to a representation that allows it. Is there an overview? |
| 2026-04-27 20:19:49 | <EvanR> | the DirStream functions in here? https://downloads.haskell.org/ghc/9.8.2/docs/libraries/unix-2.8.4.0-b036/System-Posix-Directory-PosixPath.html |
| 2026-04-27 20:20:24 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2026-04-27 20:21:59 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 20:21:59 | <haskellbridge> | <ijouw> Oh, thanks |
| 2026-04-27 20:22:03 | → | tromp joins (~textual@2001:1c00:340e:2700:144f:94ac:cf96:df60) |
| 2026-04-27 20:27:09 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-27 20:30:59 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 2026-04-27 20:31:16 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-04-27 20:36:54 | → | weary-traveler joins (~user@user/user363627) |
| 2026-04-27 20:37:19 | <janus> | Seems like hackage-server is going to use rel8 |
| 2026-04-27 20:37:31 | <janus> | now i have an excuse to learn it :) |
| 2026-04-27 20:37:48 | → | puke joins (~puke@user/puke) |
| 2026-04-27 20:38:15 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 20:40:23 | janus | . o O ( SELECT CAST(...), CAST(...) FROM (SELECT ...) LATERAL (SELECT ...) ) |
| 2026-04-27 20:41:55 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 2026-04-27 20:44:12 | × | puke quits (~puke@user/puke) (Remote host closed the connection) |
| 2026-04-27 20:44:38 | → | puke joins (~puke@user/puke) |
| 2026-04-27 20:45:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-04-27 20:47:12 | × | puke quits (~puke@user/puke) (Remote host closed the connection) |
| 2026-04-27 20:47:37 | → | puke joins (~puke@user/puke) |
| 2026-04-27 20:50:11 | × | puke quits (~puke@user/puke) (Read error: Connection reset by peer) |
| 2026-04-27 20:56:18 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 20:58:19 | × | arandombit quits (~arandombi@user/arandombit) (Remote host closed the connection) |
| 2026-04-27 20:59:11 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 272 seconds) |
| 2026-04-27 21:00:58 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-27 21:02:03 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2026-04-27 21:07:03 | × | Googulator53 quits (~Googulato@78-131-16-66.pool.digikabel.hu) (Quit: Client closed) |
| 2026-04-27 21:07:22 | → | Googulator53 joins (~Googulato@78-131-16-66.pool.digikabel.hu) |
| 2026-04-27 21:11:04 | × | tromp quits (~textual@2001:1c00:340e:2700:144f:94ac:cf96:df60) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-27 21:11:43 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 21:16:34 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-27 21:16:35 | × | r1bilski_ quits (~r1bilski@user-31-175-22-58.play-internet.pl) (Remote host closed the connection) |
| 2026-04-27 21:16:52 | → | r1bilski_ joins (~r1bilski@user-31-175-22-58.play-internet.pl) |
| 2026-04-27 21:18:49 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2026-04-27 21:22:24 | × | r1bilski_ quits (~r1bilski@user-31-175-22-58.play-internet.pl) (Ping timeout: 245 seconds) |
| 2026-04-27 21:24:11 | → | puke joins (~puke@user/puke) |
| 2026-04-27 21:25:28 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-04-27 21:27:32 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 21:30:25 | × | _________ quits (~nobody@user/noodly) (Ping timeout: 265 seconds) |
| 2026-04-27 21:32:45 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-04-27 21:36:11 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 2026-04-27 21:36:28 | → | _________ joins (~nobody@user/noodly) |
| 2026-04-27 21:37:03 | × | _________ quits (~nobody@user/noodly) (Client Quit) |
| 2026-04-27 21:38:25 | → | _________ joins (~nobody@user/noodly) |
| 2026-04-27 21:40:29 | → | emmanuelux joins (~em@user/emmanuelux) |
| 2026-04-27 21:43:20 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-27 21:46:50 | × | tok quits (~user@user/tok) (Remote host closed the connection) |
All times are in UTC.