00:00:00 --- log: started forth/21.05.08
03:18:18 --- quit: gravicappa (Ping timeout: 246 seconds)
03:19:56 --- join: gravicappa joined #forth
05:08:43 --- join: tech_exorcist joined #forth
05:15:36 --- join: cheater2 joined #forth
05:17:38 --- quit: cheater1 (Ping timeout: 265 seconds)
05:37:06 <veltas> swiftforth has shell functionality built into it and I think gforth maybe too
05:37:30 <veltas> swiftforth has a "run shell command" feature but it also has stuff like cd built in
06:02:54 --- quit: Zarutian_HTC (Read error: Connection reset by peer)
06:02:56 --- join: Zarutian_HTC1 joined #forth
06:05:20 --- quit: dave0 (Quit: dave's not here)
07:04:17 --- join: lispmacs joined #forth
07:05:02 <lispmacs> I completed this humble but fun audio project, controlling an AD9833 chip using FlashForth:
07:05:06 <lispmacs> https://librehacker.com/2021/05/07/ff-ad9833-project-musical-notes-and-melody-system-implemented/
07:09:53 <lispmacs> I've found microcontroller programming and debugging to be more fun than with any other language I've worked with. Though, of course I'd have some nice things to say about Scheme
07:12:03 <lispmacs> practically speaking, it seems easier to debug Forth code than Scheme, due to all the complicated transformations that go on in Scheme. In Guile Scheme there are back-traces but often they are difficult to read
07:13:18 <lispmacs> * microntroller programming -> microcontroller programming with Forth
08:15:58 <proteusguy> lispmacs, it is great fun, eh? :-)
08:58:46 --- quit: Vedran (Ping timeout: 268 seconds)
09:32:17 <siraben> lispmacs: hm, I find the Guile backtraces pretty helpful
09:32:41 <siraben> or maybe I spent most of my Forth programming debugging in my own implementation, so naturally it had poor debugging heh
09:33:16 <siraben> lispmacs: oh is that your blog?
09:34:07 --- quit: Zarutian_HTC1 (Read error: Connection reset by peer)
09:59:31 --- join: Zarutian_HTC joined #forth
10:39:49 <lispmacs> siraben: yes
11:00:52 --- join: Vedran joined #forth
11:18:35 <KipIngram> lispmacs: Embedded is a lot of fun.  I've always enjoyed it.  I particularly revel in having control over all of the hardware AND all of the software - the whole process of making them "cooperate" to get something done is just pleasant.
11:18:48 <KipIngram> And Forth really is a GREAT embedded tinkering language.
11:19:02 <KipIngram> Close to perfect.
11:26:25 <KipIngram> So, I've been thinking about this numeric output stuff some more.  At any given moment, if I had a number sitting on the stack, I could execute Forth to output it in some particular format.  So I think the way to structure this is to let the format fields just be an alternative way of encoding a stream of normal Forth words.  When I come to a format field, I just trigger a little byte code interpreter and it
11:26:26 <KipIngram> will produce the same steps I might write in Forth.
11:26:56 <KipIngram> Byte code was the way I did it before, but it was a little different - I had no idea of the byte code actually representing Forth in a very specific way.
11:27:48 <KipIngram> In particular, there was no concept of "looping over the byte code."  The byte code really just managed the acquisition of numeric parameters for the conversion, and then the last character triggered a word that did the whole job.
11:28:11 <KipIngram> This time I'm going to explore having the byte code actually encode all the work, in a very explicit way, with loops and the whole shebang.
11:28:19 <KipIngram> See which way turns out better.
11:29:06 <KipIngram> It may turn out that doing that way makes the format field too complex.
11:30:02 <KipIngram> I actully think that's fairly likely.
11:59:31 <KipIngram> But I think there may be a nice "collaboration" of the previous byte code interpreter idea with my new way of using stack frames, that could make the whole process a little more elegant.
12:19:38 --- join: LispSporks joined #forth
12:31:53 --- quit: gravicappa (Ping timeout: 260 seconds)
12:39:51 --- quit: LispSporks (Quit: My MacBook has gone to sleep. ZZZzzz…)
14:05:26 --- quit: proteus-guy (Ping timeout: 265 seconds)
14:13:59 --- quit: wineroots (Remote host closed the connection)
14:17:24 --- join: proteus-guy joined #forth
14:20:07 * tabemann has life running on his F7 board, displayed over swdcom as sixels
14:22:38 <KipIngram> Cool.  :-)
14:33:45 <tabemann> next thing to do: display it on the screen that comes with the F7 DISCO
14:35:28 --- quit: tech_exorcist (Ping timeout: 268 seconds)
14:35:49 --- quit: spoofer (Quit: Lost terminal)
14:36:26 <tabemann> I should make a modification so it can display four pixels per cell rather than one pixel
14:36:33 <tabemann> because one pixel is pretty tiny
14:39:12 --- join: LispSporks joined #forth
14:46:26 --- join: spoofer joined #forth
15:09:04 --- quit: proteus-guy (Ping timeout: 252 seconds)
15:21:55 --- join: proteus-guy joined #forth
15:22:43 <tabemann> now my sixel support uses RLE
15:34:50 <Zarutian_HTC> nice!
15:37:02 <KipIngram> Oh... That DISCO board looks pretty sweet.
15:37:13 <KipIngram> That's a nice roomy display.
15:37:25 <KipIngram> Is it a touch screen?
15:39:07 <KipIngram> Oh, it IS.
15:39:10 <KipIngram> Very sweet.
15:39:23 <KipIngram> Plenty of flash and RAM for a Forth to go to town in, too.
15:40:21 --- quit: LispSporks (Quit: My MacBook has gone to sleep. ZZZzzz…)
15:53:20 <sts-q> Bruder Jakob, 
15:53:21 <sts-q> Bruder Jakob,
15:53:21 <sts-q> schläfst du noch, 
15:53:21 <sts-q> schläfst du noch,
15:53:21 <sts-q> hörst du nicht die Glocken
15:53:21 <sts-q> hörst du nicht die Glocken
15:53:22 <sts-q> bim bam bom
15:53:22 <sts-q> bim bam bom
15:54:01 <sts-q> iloveit :))
16:03:36 <sts-q> https://www.youtube.com/watch?v=Mfsnlbd-4xQ
16:11:54 <sts-q> https://www.youtube.com/watch?v=yY1FSsUV-8c&t=96s
16:19:41 --- join: LispSporks joined #forth
16:19:43 --- quit: LispSporks (Client Quit)
16:19:47 <sts-q> never ever compare ( just enjoy )
16:21:48 <tabemann> back
16:22:54 <tabemann> the only problem with my forth impl is that it's kinda slow
16:24:06 <KipIngram> Any thoughts about what slows it down?
16:37:06 <tabemann> well, it's running at 216 mhz, and it's shoving bytes through swdcom, which uses a 255 byte buffer
16:37:26 <tabemann> of course, using serial wouldn't be any faster for sure
16:38:08 <tabemann> even then, I tried to speed it up using sixels' RLE compression, and while that has helped to a degree, it's still slowish
16:42:22 <KipIngram> Oh, ok - so it's not necessarily slow executing - it's got some heavy I/O to do.
16:52:24 --- quit: proteus-guy (Ping timeout: 246 seconds)
16:59:19 --- join: dave0 joined #forth
17:00:00 <dave0> maw
17:04:53 --- join: proteus-guy joined #forth
17:07:35 <tabemann> I just wrote a test which runs life without displaying anything other than a cycle count
17:07:46 <tabemann> and it's still slowish
17:07:56 <tabemann> this is with a 160x160 world
17:08:47 <tabemann> it runs much faster with a 80x80 world
17:09:48 <KipIngram> Does it redraw the whole world each frame?
17:12:22 <tabemann> when it's running in display mode, yes
17:14:16 <KipIngram> So even when you display just the cycle count, you're still computing the new worlds?  Just not sending them to the display?
17:20:28 <KipIngram> What are your turn on/turn off rules?
17:20:42 <KipIngram> Do diagonal neighbors count, or just rectangular ones?
17:24:14 <KipIngram> I'm just wondering if there might be a way to do the bitmap update using byte-size calculations, maybe with some tables.
17:24:58 <dave0> tabemann: if you really wanted to be perverse, you could use SIMD :-)
17:25:11 <dave0> count the number of neighbors in parallel
17:25:15 <dave0> :-)
17:26:04 <KipIngram> It just feels like a "ripe problem" for some parallel exploits.
17:28:16 <KipIngram> If you got 160 bytes per row, then above and below neighbors are always exactly 20 bytes away, in the same bit location.
17:28:39 <KipIngram> The left and right neighbor calculations could likely be rolled into a 256-byte table.
17:29:16 <KipIngram> It would be the LSB and the MSB bits that would be the most noxious - you'd actually have to look at those neighbors, and would only get one bit's worth of information from each look.
17:29:51 <KipIngram> And I guess there would be 3200 of those.
17:30:31 <dave0> oh oh you're representing the grid as an array of bits?
17:30:40 <KipIngram> I don't know - I'm presuming.
17:30:43 <KipIngram> He hasn't told us.
17:30:49 <dave0> ah okay
17:31:46 <dave0> using bits would definately keep things small.. you could have massive boards
17:33:02 <KipIngram> Well, he said earlier each cell was a pixel, and that he was considering going to 2 pixels by 2 pixels to make them bigger.
17:33:17 <KipIngram> So I assume right now it's a bit-built thing.
17:34:44 <KipIngram> But you could get the horizontal update for all six internal bits of a byte from a table lookup.  And then another table lookup could get the above contribution, and another the below contribution.
17:35:03 <KipIngram> So that would just leave the LSB and MSB of every byte, the left and right contributions.
17:49:45 <Zarutian_HTC> to improve locality one could use a hilbert curve layout of the board in memory
17:50:51 <Zarutian_HTC> but that aint as easy to calculate locations relative to
17:51:34 <Zarutian_HTC> as say the usual stride method of progressive 'scanline' layout usually used
17:52:14 --- quit: mark4 (Quit: Leaving)
17:54:52 --- join: mark4 joined #forth
17:55:17 --- mode: ChanServ set +v mark4
18:09:21 --- quit: dave0 (Quit: dave's not here)
18:11:33 <KipIngram> I'd have to look that up.  I vaguely knnow what Hilber curves are, but certainly don't have them readily at mind.
18:17:11 <KipIngram> Hilbert
18:17:20 <KipIngram> Space filling, right?
18:19:04 <KipIngram> What's the exact rule?
18:19:43 <KipIngram> Is it an even/odd thing?  A majority?  Feels like even/odd would work better.
18:22:43 <KipIngram> Ah, Wikipedia says all eight neighbors count.  That's much more involved, I think.
18:39:07 <KipIngram> At least that F7 DISCO board supports some non-windows toolchains.  It really steams me up when people put out cool little products but only offer Windows support.
18:39:14 <KipIngram> It's like... OSist.
18:39:39 <KipIngram> I hate seeing Microsoft being given further advntages.
18:45:35 --- join: boru` joined #forth
18:45:38 --- quit: boru (Disconnected by services)
18:45:40 --- nick: boru` -> boru
18:49:04 <KipIngram> There is some interesting information here:
18:49:06 <KipIngram> https://stackoverflow.com/questions/5059817/whats-an-efficient-implementation-of-conways-game-of-life-for-low-memory-uses
18:49:25 <KipIngram> See the answer by David Cary
18:54:46 --- join: LispSporks joined #forth
18:55:27 --- quit: LispSporks (Client Quit)
18:56:16 <KipIngram> Hey, sometime a year ago or so someone here had a "rotating PAD" implementation.
18:56:39 <KipIngram> PAD moved around a circular buffer, so you didn't just immediately overwrite its previous content.
18:56:58 <KipIngram> It would only get overwritten when you used it enough to wrap bye buffer around.
18:57:03 <KipIngram> Sound familiar to anyone?
18:57:34 <KipIngram> I'm thinking of doing something similar to provide a reasonably clean way to work with strings.
18:57:57 <KipIngram> I'd have pointers into the circular buffer and manipulate them on the stack.
18:59:47 <tabemann> back
19:00:34 <KipIngram> Ah, we've been talking behind your back - you may find a scrollback interesting if you've got it.
19:01:09 <tabemann> oh, and when I'm just displaying the cycle count, I am computing new worlds
19:01:21 <KipIngram> I figured you probably were.
19:02:01 <KipIngram> Do you wrap your edges to one another?
19:02:08 <tabemann> yes
19:02:21 <tabemann> and yes, I'm treating the grid as an array of bits
19:02:24 <KipIngram> Ok, so you're basically simulating a donut.  Torroidl geometry.
19:02:31 <KipIngram> Toroidal
19:02:36 <tabemann> it would be faster if I treated it as a grid of bytes
19:02:46 <tabemann> but then it would use eight times as much memory
19:03:12 <KipIngram> Right.  I posted a link to a discussion that had some other places to look for fast ways to do it.
19:03:29 <tabemann> the fast way to implement it is hashlife
19:05:18 <KipIngram> Oh... hashlife looks interesting.
19:16:14 <KipIngram> Are you going to try to use a Life board to do any computing?
19:16:33 <KipIngram> I saw a game of life once running a game of life.
19:16:58 <tabemann> interesting
19:17:29 <tabemann> nah, I can't really use life on here to do anything really interesting, as even though it's an F7 it's still too limited by speed and memory
19:18:06 <KipIngram> Well, it's purely an academic thing to do anyway.
19:18:15 <KipIngram> It's not the way anyone would ever do anything, but it's... "cute."
19:19:00 --- quit: Keshl (Read error: Connection reset by peer)
19:22:25 --- quit: Zarutian_HTC (Read error: Connection reset by peer)
19:22:45 --- join: Zarutian_HTC joined #forth
19:24:35 --- join: Keshl joined #forth
19:31:28 --- quit: sts-q (Ping timeout: 268 seconds)
19:45:04 --- join: sts-q joined #forth
20:42:25 --- join: dave0 joined #forth
20:46:51 <dave0> maw
20:50:05 <KipIngram> Hi dave0.
20:52:31 --- join: gravicappa joined #forth
20:54:38 <dave0> maw KipIngram !
21:02:06 --- quit: spoofer (Remote host closed the connection)
21:05:22 --- join: spoofer joined #forth
21:19:43 <siraben> remexre: it was clear I would need something more nuanced than final states for Forth program equivalence 
21:19:55 <siraben> so I should look into bisimulation
21:20:37 <remexre> huh, where'd you get stuck?
21:20:50 <siraben> I wasn't even able to show `p skip` is equivalent to `p`
21:21:23 <remexre> `p skip q` should always be equivalent to `p q` though, right?
21:21:32 <remexre> like that one ought to be "showable"
21:21:47 <remexre> easily provable*
21:22:04 <siraben> actually I was able to show `Theorem simulates_skip2 : forall p, simulates <{ skip p }> p.` and `Theorem simulates_skip : forall p, simulates p <{ skip p }>.`
21:22:20 <siraben> `Definition simulates (p q : com) := ∀ (st st' : stack) (p' : com), p / st --> p' / st' -> ∃ q', q / st -->* q' / st'.`
21:22:47 <siraben> (ok this is technically wrong because the use of star suggests q could take zero steps and you have an infinite stuttering problem)
21:23:08 <siraben> but that's the idea, "if p can take a step then q can take zero or more steps to end up in the same state as p"
21:23:13 <siraben> `Definition bisimulates (p q : com) := simulates p q /\ simulates q p.`
21:23:43 <remexre> hm, why isn't it -->* on both sides?
21:23:46 <siraben> actually wait, if q takes zero steps then st = st', which may not be true
21:24:15 <siraben> Oh I think it's because if I have -->* on the hypothesis, I'd have to induct over it?
21:24:20 <siraben> like, it may actually be 0 steps
21:25:04 <remexre> hm
21:25:08 <siraben> I'm basing it roughly on https://homes.cs.washington.edu/~djg/msr_russia2012/sangiorgi.pdf
21:25:30 <remexre> isn't simulates <{ skip p }> <{ p incr }> inhabited though?
21:25:35 <siraben> and https://xavierleroy.org/courses/EUTypes-2019/slides.pdf
21:25:47 <remexre> uhoh coinduction
21:26:33 <siraben> yeah I'd probably have to read CPDT to know more about coinduction heh
21:29:25 <siraben> Let me try inhabiting that
21:32:18 <siraben> remexre: oh crap, you are right
21:32:29 <siraben> `intros p st st' p' H. inversion H; subst. eexists; auto. inversion H1.` proves it
21:32:33 <siraben> uh oh
21:32:36 <remexre> I think you might want a length-indexed version of -->*
21:33:19 <siraben> yeah, slide 66 of the xavierleroy presentation "Find a measureM(s) :natover source terms that decreases strictly whena stuttering step is taken. Then show:"
21:33:36 <siraben> bah, then something I should do only after finals
21:33:51 <siraben> is that what you meant by length indexed?
21:33:54 <remexre> and say something like, forall n, exists m, (p / st -->*# p / st') n -> (q / st -->*# q / st') m
21:34:15 <remexre> where (a -->*# b) n = "exactly n steps of (a --> b)"
21:34:41 <siraben> also exists q?
21:34:55 <siraben> I mean q'
21:35:11 <remexre> er yeah, I accidentally dropped the ' on p' and q'
21:36:19 <remexre> really you just need, forall n, (p / st -->*# p' / st') -> exists q', (q / st -->* q' / st')
21:36:53 <remexre> but if you're making -->*# you could just define (a -->* b) := (exists n, (a -->*# b) n)
21:37:31 <siraben> Right.
21:41:03 <remexre> oh, this is slide 30 of ~djg's presentation, I think
21:41:10 <remexre> at least, I think that's what the mu is?
21:41:25 <remexre> wait, no
21:41:37 <remexre> shouldn't need be the same number of steps on each side
21:42:38 <remexre> oh, mu is a trace, I think
21:50:09 <siraben> remexre: mu is a label of a transition system
21:50:16 <remexre> ah
22:21:40 --- quit: proteus-guy (Ping timeout: 268 seconds)
22:34:52 --- join: proteus-guy joined #forth
23:59:59 --- log: ended forth/21.05.08