Logs: liberachat/#haskell
| 2021-06-28 12:06:39 | → | azeem joins (~azeem@176.201.40.58) |
| 2021-06-28 12:07:47 | → | safinaskar joins (~safinaska@109-252-90-89.nat.spd-mgts.ru) |
| 2021-06-28 12:09:49 | → | acarrico joins (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) |
| 2021-06-28 12:12:59 | <safinaskar> | I want some logical framework, which can handle arbitrary logics. Ideally, description format for logics should be as close as possible to what we see in mathematical papers (for example, see how simply typed lam. cal. defined here: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus ). In other words, description format should be similar to |
| 2021-06-28 12:13:00 | <safinaskar> | what we have in ott-lang. Now let me say what I don't like in existing logical frameworks. Ott-lang - this is not logical framework, nor a prover, it simply converts its input to other forms, and ott's docs warn users that this conversion is unreliable. Automath, Twelf - too simple, i think all its features can be simply replaced by haskell's or |
| 2021-06-28 12:13:00 | <safinaskar> | agda's GADTs |
| 2021-06-28 12:13:51 | <Arahael> | Is Apple M1 still "not supported"? |
| 2021-06-28 12:14:51 | <safinaskar> | boxscape: ok, thanks for answer! |
| 2021-06-28 12:15:48 | <Hecate> | Arahael: https://www.haskell.org/ghc/blog/20210309-apple-m1-story.html |
| 2021-06-28 12:17:00 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Ping timeout: 272 seconds) |
| 2021-06-28 12:17:47 | × | acarrico quits (~acarrico@dhcp-68-142-39-249.greenmountainaccess.net) (Ping timeout: 268 seconds) |
| 2021-06-28 12:18:04 | <Arahael> | Hecate: Ah, so not /quite/ yet, but "soon"! Thanks for the link, though, it was a good read. |
| 2021-06-28 12:18:29 | <Hecate> | Arahael: you're welcome. :) You can thank bgamari & angerman |
| 2021-06-28 12:19:50 | <Arahael> | For sure. Looks like there's been a _huge_ amount of work involved. |
| 2021-06-28 12:19:58 | <angerman> | Arahael: actually it *is* supported. |
| 2021-06-28 12:20:32 | <angerman> | 8.10.5 has support for it via LLVM. But there are some issues with 8.10.5, so there will be a 8.10.6 release. |
| 2021-06-28 12:20:51 | <angerman> | Arahael: 9.2 will come with a NCG for aarch64-darwin. |
| 2021-06-28 12:23:27 | <angerman> | Arahael: for some recent fun debugging GHC on aarch64-darwin (M1) see https://twitter.com/angerman_io/status/1409459100463734792 |
| 2021-06-28 12:24:06 | <Arahael> | angerman: Ah, awesome. The website probably needs to be updated, then? |
| 2021-06-28 12:24:46 | <angerman> | I guess I should pressure Ben into adding an update :-) |
| 2021-06-28 12:25:22 | <Arahael> | angerman: You should! :D |
| 2021-06-28 12:26:11 | <angerman> | Arahael: we’ll the summary kinda says that 8.10.5 will have M1 support. And that 9.2.1 will come an NCG ;-) |
| 2021-06-28 12:26:57 | <Arahael> | angerman: I just saw that it was "not supported" right on https://www.haskell.org/downloads/#linux-mac-freebsd |
| 2021-06-28 12:26:59 | <angerman> | It doesn’t really help that apple calls aarch64 “arm64” and then went overboard with thr M1 branding :-/ |
| 2021-06-28 12:27:30 | <angerman> | Ohh lovely yet another page :-) |
| 2021-06-28 12:27:46 | <Arahael> | angerman: Yeah, well, I can understand the M1 branding - supposedly it features a memory mode that lets them emulate the x86 code more efficiently. |
| 2021-06-28 12:28:15 | <Arahael> | angerman: I just literally went: haskell.org -> Downloads -> Linux, OS X and Free BSD! |
| 2021-06-28 12:28:27 | <Arahael> | I must be the only one who uses teh main website in this community! :D |
| 2021-06-28 12:28:32 | <angerman> | Arahael: completely understandable |
| 2021-06-28 12:29:09 | <Arahael> | :) |
| 2021-06-28 12:29:12 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 2021-06-28 12:29:21 | <angerman> | Arahael: I just build all my compilers from source anyway, I believe your path is taken by quite a few actually. |
| 2021-06-28 12:30:22 | <angerman> | Arahael: yes. The M1 comes with some features that make Rosetta easier. But when people ask for M1 support they usually mean “native” AArch64/darwin :-) |
| 2021-06-28 12:31:02 | → | oxide joins (~lambda@user/oxide) |
| 2021-06-28 12:31:53 | × | berberman quits (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-06-28 12:32:50 | → | jao joins (~jao@cpc103048-sgyl39-2-0-cust502.18-2.cable.virginm.net) |
| 2021-06-28 12:32:54 | → | berberman joins (~berberman@user/berberman) |
| 2021-06-28 12:33:10 | × | Feuermagier quits (~Feuermagi@user/feuermagier) (Ping timeout: 252 seconds) |
| 2021-06-28 12:33:19 | <Arahael> | angerman: Indeed. :) |
| 2021-06-28 12:33:55 | <Arahael> | angerman: Yeah, I prefer to grab binaries for the most part. I flit from language to language and arch too often. :( |
| 2021-06-28 12:35:04 | <angerman> | Perfectly fine. Arahael, maerwald’s ghcup might be for you :-) |
| 2021-06-28 12:36:17 | ← | jakalx parts (~jakalx@base.jakalx.net) (Error from remote client) |
| 2021-06-28 12:36:22 | <Arahael> | Nice - interesting, so that works with macos as well? I should get to be. |
| 2021-06-28 12:36:23 | <Arahael> | *bed. |
| 2021-06-28 12:37:38 | <Arahael> | Thanks for the links though, I'll be reading the off-by-one error in particular :) |
| 2021-06-28 12:37:40 | → | jakalx joins (~jakalx@base.jakalx.net) |
| 2021-06-28 12:37:47 | → | chomwitt joins (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4) |
| 2021-06-28 12:39:02 | × | dunkeln quits (~dunkeln@188.71.193.140) (Ping timeout: 268 seconds) |
| 2021-06-28 12:39:39 | → | berberman_ joins (~berberman@user/berberman) |
| 2021-06-28 12:40:32 | → | dunkeln joins (~dunkeln@188.71.193.140) |
| 2021-06-28 12:40:36 | × | berberman quits (~berberman@user/berberman) (Ping timeout: 268 seconds) |
| 2021-06-28 12:41:04 | × | haykam1 quits (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-06-28 12:41:18 | → | haykam1 joins (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-06-28 12:47:48 | × | azeem quits (~azeem@176.201.40.58) (Ping timeout: 258 seconds) |
| 2021-06-28 12:47:54 | <dminuoso> | 14:46:54 boxscape_ | [10:00:15] what would you use for number things |
| 2021-06-28 12:48:00 | <dminuoso> | Potentially FORTRAN. |
| 2021-06-28 12:48:15 | → | mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
| 2021-06-28 12:48:36 | <dminuoso> | BLAS or LAPACK are neat for linear algebra |
| 2021-06-28 12:49:10 | <dminuoso> | FORTRAN has this weird habit of still being used widely in lots of number crunching for having quite a few high performance libraries. |
| 2021-06-28 12:51:17 | × | trcc quits (~trcc@2-104-60-169-cable.dk.customer.tdc.net) (Remote host closed the connection) |
| 2021-06-28 12:51:54 | → | trcc joins (~trcc@2-104-60-169-cable.dk.customer.tdc.net) |
| 2021-06-28 12:52:24 | → | Feuermagier joins (~Feuermagi@user/feuermagier) |
| 2021-06-28 12:52:29 | → | pbrisbin joins (~patrick@pool-173-49-147-28.phlapa.fios.verizon.net) |
| 2021-06-28 12:53:01 | → | azeem joins (~azeem@176.201.40.58) |
| 2021-06-28 12:53:32 | × | Reyu[M] quits (~reyureyuz@matrix.reyuzenfold.com) (Remote host closed the connection) |
| 2021-06-28 12:54:17 | → | Reyu[M] joins (~reyureyuz@matrix.reyuzenfold.com) |
| 2021-06-28 12:54:50 | → | jolly joins (~jolly@208.180.97.158) |
| 2021-06-28 12:54:55 | × | trcc quits (~trcc@2-104-60-169-cable.dk.customer.tdc.net) (Read error: Connection reset by peer) |
| 2021-06-28 12:55:27 | → | trcc joins (~trcc@2-104-60-169-cable.dk.customer.tdc.net) |
| 2021-06-28 12:56:42 | × | qoelet quits (~kumo@139.180.144.166) (Ping timeout: 240 seconds) |
| 2021-06-28 12:59:47 | × | cheater quits (~Username@user/cheater) (Ping timeout: 250 seconds) |
| 2021-06-28 12:59:48 | × | Scotty_Trees quits (~Scotty_Tr@162-234-179-169.lightspeed.brhmal.sbcglobal.net) (Quit: Leaving) |
| 2021-06-28 13:00:08 | → | hmmmas joins (~chenqisu1@183.217.200.246) |
| 2021-06-28 13:00:28 | → | cheater joins (~Username@user/cheater) |
| 2021-06-28 13:01:12 | → | alx741 joins (~alx741@181.196.69.41) |
| 2021-06-28 13:05:06 | × | mikoto-chan quits (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) (Read error: No route to host) |
| 2021-06-28 13:05:08 | × | MQ-17J quits (~MQ-17J@d14-69-206-129.try.wideopenwest.com) (Ping timeout: 272 seconds) |
| 2021-06-28 13:05:32 | → | mikoto-chan joins (~mikoto-ch@ip-213-49-189-31.dsl.scarlet.be) |
| 2021-06-28 13:05:55 | × | jneira quits (~jneira@212.8.115.226) (Quit: Client closed) |
| 2021-06-28 13:07:17 | → | MQ-17J joins (~MQ-17J@d14-69-206-129.try.wideopenwest.com) |
| 2021-06-28 13:10:06 | → | berberman joins (~berberman@user/berberman) |
| 2021-06-28 13:11:26 | × | berberman_ quits (~berberman@user/berberman) (Ping timeout: 268 seconds) |
| 2021-06-28 13:12:12 | → | chris_ joins (~chris@81.96.113.213) |
| 2021-06-28 13:12:30 | × | juhp quits (~juhp@bb116-14-48-29.singnet.com.sg) (Quit: juhp) |
| 2021-06-28 13:12:45 | → | juhp joins (~juhp@bb116-14-48-29.singnet.com.sg) |
| 2021-06-28 13:14:38 | × | cheater quits (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-06-28 13:15:07 | → | fizbin joins (~fizbin@c-73-33-197-160.hsd1.nj.comcast.net) |
| 2021-06-28 13:15:10 | → | cheater joins (~Username@user/cheater) |
| 2021-06-28 13:15:16 | → | warnz joins (~warnz@2600:1700:77c0:5610:eca1:bc9d:4345:931f) |
| 2021-06-28 13:16:08 | ← | safinaskar parts (~safinaska@109-252-90-89.nat.spd-mgts.ru) () |
| 2021-06-28 13:16:22 | → | xsperry joins (~as@user/xsperry) |
| 2021-06-28 13:16:22 | × | dunkeln quits (~dunkeln@188.71.193.140) (Ping timeout: 268 seconds) |
| 2021-06-28 13:18:28 | × | berberman quits (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2021-06-28 13:19:26 | → | berberman joins (~berberman@user/berberman) |
| 2021-06-28 13:19:37 | × | hmmmas quits (~chenqisu1@183.217.200.246) (Quit: Leaving.) |
| 2021-06-28 13:20:06 | × | warnz quits (~warnz@2600:1700:77c0:5610:eca1:bc9d:4345:931f) (Ping timeout: 272 seconds) |
| 2021-06-28 13:20:13 | × | jespada quits (~jespada@90.254.247.46) (Ping timeout: 265 seconds) |
| 2021-06-28 13:23:04 | → | jespada joins (~jespada@90.254.247.46) |
| 2021-06-28 13:25:00 | × | azeem quits (~azeem@176.201.40.58) (Ping timeout: 268 seconds) |
| 2021-06-28 13:25:17 | × | berberman quits (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
All times are in UTC.