00:00:00 --- log: started forth/21.05.04 00:38:04 So what can You possibly get with Arduino!? A punishment (that it is)!? 00:42:20 --- join: mtsd_ joined #forth 00:44:42 --- quit: mtsd (Ping timeout: 246 seconds) 01:17:21 --- quit: wineroots (Read error: Connection reset by peer) 01:17:32 --- quit: mtsd_ (Ping timeout: 252 seconds) 01:18:54 --- join: wineroots joined #forth 01:19:01 --- join: mtsd joined #forth 02:09:01 --- quit: dave0 (Quit: dave's not here) 03:29:05 --- join: proteus-guy joined #forth 03:38:42 --- join: andrei-n joined #forth 03:54:53 --- quit: andrei-n (Read error: Connection reset by peer) 04:14:58 --- join: andrei-n joined #forth 04:48:11 --- quit: mtsd (Ping timeout: 252 seconds) 04:56:49 --- join: mtsd joined #forth 06:18:47 --- join: tech_exorcist joined #forth 06:27:11 --- quit: Zarutian_HTC (Ping timeout: 252 seconds) 07:40:43 --- join: actuallybatman joined #forth 08:03:42 Zarutian_HTC: I suppose you good, but how precise would it be? 08:05:25 could 08:09:02 What do you cut your soda can with? 09:12:31 --- quit: mark4 (Remote host closed the connection) 09:12:52 --- join: mark4 joined #forth 10:26:35 --- quit: lispmacs[work] (Read error: Connection reset by peer) 10:29:17 --- join: lispmacs[work] joined #forth 10:43:54 --- quit: gravicappa (Ping timeout: 246 seconds) 10:49:59 A good stencil is a precision piece of gear - if the stencil is sloppy it can cause all manner of problems. 10:56:09 Hey, it occurs to me that Forth doesn't really provide a "conventional" way of accessinng the instruction stream, does it? It's easy to do from primitives, but there's not really a way to access that value from Forth itself, is there? 10:56:30 Oh wait - never mind. 10:56:42 Of course there is - in a colon definition that will be on top of the return stack. 10:56:44 Duh... 10:58:55 I was thinking about getting at the actual IP, but now I can't thinkn of a reason one would ever want that. 11:16:28 what type of assessment are you trying to do? 11:16:59 MrMobius: Was that aimed at me? 11:18:34 I was just thinking about accessing inline arguments. Primitives can do it easily, since they can use the IP register to address the arg. I was wondering if there was an equivalent ability "at the Forth level," and of course there is - if you call a Forth word then the address of the argument gets pushed onto the return stack and you've got to bump it forward before returning. 11:18:39 So it was a dumb question. 11:18:49 Induced by lack of caffeine. 11:20:43 KipIngram, yes 11:20:58 I can't really think of a case where you'd need the actual IP in Forth - annytime you are in a position to act on it it's been pushed to the return stack. 11:27:24 I made this change to my system yesterday, where there's a bit in the header that will instruct the compiler to compile the usual word call but then follow it with a byte offset back to the start of the definition. 11:27:46 It was to avoid having to write immediate wrappers for all of my plethora of conditional looping words. 11:28:11 I realized this morning that I'll also be able to use that bit for words I define, so long as I provide a way of setting it. 11:29:04 I don't particularly like complicating the compiler - probably a slippery slope. But I particularly HATED the idea of 41 extra immediate words in my dictionary. 11:30:32 So what this is boiling down to is that in my Forth there's only ever one jump target: back to the start of the word. 11:31:02 I don't have IF ... THEN and so on that specify other jump targets. 11:32:00 So all of my loops are essentially tail recursion loops, though in a few places I don't do it just at the tail. 11:33:52 In several places I have infinite tail recursion loops, but then there will be a conditional return somewhere in the loop body. 11:33:59 That's how I get out. 11:39:30 It simplifies the system to do it that way - makes it so the jump target is always available via LATEST. 11:39:47 Doesn't have to be noted on the stack, paired with a code of some kind. 11:43:47 Another thing I do in the compiler is each time I tick a word into the dictionary I remember it in a variable. ; uses that to do tail optimization - basically if the CFA of the word points to (:) / docol then it does the tail optimization - if it doesn't, it doesn't. 11:44:28 Also execution of an immediate word would clear that variable - that took care of the case where you don't want to tail optimize here: 11:44:46 : foo ... IF ... <: word> THEN ; 11:45:03 You can't tail optimize that, because there has to be something down there for the IF to jump to. 11:46:44 It will be the ; runntime if you don't optimize, and things will be happy. 11:47:15 But if you tail optimize it then the last thing in the definition will be a jump to <: word>, and that's part of what you want to skip over if the IF jumps. 11:47:41 Since I don't use IF THEN anymore I don't have that case to worry about. 11:48:58 Storing that variable was the resolution of a lot of scratching around trying to figure out when to optimize and when not to solely by looking at what I'd just compiled. You can't - because for all you know something back upstream will try to jump over that last word to the ; runtime. You have to have more global knowledge in order to do it right. 11:51:46 "Global knowledge" of the whole compile process just isn't something Forth excels at offering you. 11:59:11 The other problem with just trying to look at the last cell to see if it designates a : definition is that it could be a literal number, and that means it could have any value whatsoever. 11:59:34 Including one that WOULD be a : def, if it weren't a number. 11:59:52 So you really must have a small bit of state. 12:00:31 If you actually put a : def word into the definition (and you can be sure of it WHEN YOU'RE DOING IT), set the state; if you put anything else in the dictionary clear the state. 12:00:37 Then ; knows what to do. 12:21:44 So, the changes yesterday to my flags enabled these definitions for nfa and lfa (starting form cfa): 12:21:54 : nfa 1- .c@ x:80 and 0=me ; 12:21:59 : lfa nfa 2- ; 12:46:14 --- join: logand joined #forth 12:58:30 --- quit: andrei-n (Quit: Leaving) 13:27:33 --- quit: mtsd (Ping timeout: 240 seconds) 13:32:35 I think I got all the nuances of the interpret/compile code straightened out now. Time to let it sit there in front of me for a few days. 13:33:15 It handles the creation of that tail optimization state and also adds the offset after words that have that loop bit set in the header. 13:34:13 When I parse words from the input stream the place I store them is where they will need to be if they become part of the dictionary. So CREATE will just need to add some info in around that data and adjust some pointers. 13:47:58 --- join: Zarutian_HTC joined #forth 14:04:25 --- join: dave0 joined #forth 14:05:35 --- quit: tech_exorcist (Ping timeout: 268 seconds) 14:06:20 maw 14:22:52 --- join: pointfree joined #forth 15:24:33 So, when I recompile my system, it's not only the base addresses and dictionary pointers I need to switch to an "image area." I need for everything to go there. The search path and the contents of CURRENT have to refer to the image as well. 15:24:59 But I probably need access to my system search path as well. 15:25:19 This needs some careful thought before I box myself into a corner. 15:25:48 It feels like one of those things that could go very well if it's approached right, but become a nightmare if it's not. 15:27:19 And this stuff I've just coded may be affected. 16:31:04 --- quit: Vedran (Quit: Ping timeout (120 seconds)) 16:31:29 --- join: Vedran joined #forth 16:49:02 --- quit: pointfree (Quit: Connection closed for inactivity) 17:03:48 --- quit: dave0 (Quit: dave's not here) 17:22:46 Ok, so after thinking about it for a while, I think that all I need to do is change all of those variables (base addresses, here variables, context, current) and then launch into compiling the system and never come back to the console until it's all done and I've restored the variables. 17:23:05 That way if an error occurs at any point, my error recovery will restore those variables using the recovery image. 17:24:04 I'll want the virtual instruction words that generate target code to be part of my host system - I'll actually be executing those words while building target primitives. But everything beyond that will get looked up in the target dictionary. 17:27:57 All I really need to do to make this work is make sure thaat I don't use the register copies of the base addresses for compiling. Always the variable version, so that I can change them. But the proper RUNNING of the system never relies on those variables - the registers just have to be right. 17:28:06 So it all should work just fine. 17:35:29 --- join: cheater joined #forth 17:35:38 insert may the forth joke here 17:38:57 back 17:39:03 hey guys 17:40:11 --- join: logand` joined #forth 17:42:02 --- quit: logand (Ping timeout: 252 seconds) 17:46:05 Hey tabeman... 18:23:04 --- quit: lispmacs[work] (Remote host closed the connection) 18:50:14 --- join: boru` joined #forth 18:50:17 --- quit: boru (Disconnected by services) 18:50:20 --- nick: boru` -> boru 19:08:52 --- join: LispSporks joined #forth 19:12:39 --- join: dave0 joined #forth 19:14:04 maw 19:18:27 remexre: I thought up of a small-step operational semantics for a Forth-like language 19:18:52 it occurred to me that Hoare logic could be used as well to decorate the programs, instead of variables you would use stack offsets (like de bruijn indices) 19:19:37 then you could truly assert something like, `{ #0 = n } FACT { #0 = fact n }` for a program that calculates factorial 19:21:28 ooh, nice 19:22:15 I would make constructs like REPEAT, WHILE etc. primitive however 19:22:22 then compile to a stack-baesd VM with jumps and all that 19:23:28 until I'm familiar with proving fiddly things about such a machine, I'll stick to that higher-level smallstep operational semantics 19:23:46 remexre: wrt. conditions, should the stack be typed then? 19:24:08 conditions as in CL conditions? 19:24:09 conditionals* 19:24:14 ah 19:24:43 my personal view for what I'm doing in my forth is, it's more useful to have the stack "types" instead be predicates on machine state 19:25:07 Ah ok, so the conditionals just operate on numbers rather than booleans? 19:25:13 yeah 19:26:30 I see. So `state = list nat` then 19:28:06 so I'm planning to do mine over the whole state of an aarch64 CPU 19:28:16 and then have a helper to get the stack's contents 19:29:16 but if your forth doesn't have a stack accessible as memory (and has unbounded nats for values!) then sure 19:29:24 Oh I see. I prefer to start more idealistic then gradually add more realism to the formalization 19:30:17 with nats as values on the stack, it'd be a very unique Forth for sure, haha 19:30:25 yeah, I'll probably do a trial run with a simpler "model" of a forth, where each primitive is one instruction, no paging exists, things are at nice small-numbered addresses, etc 19:31:30 but I'll probably try to have the stack in memory all the time, because that's like, a really big change 19:32:53 it sounds tougher to formalize things when the stack is also in memory 19:33:05 like, you'd have to bound the height of the stack to prevent collisions? 19:33:13 yeah 19:33:23 but I should know what stack depth each primitive needs 19:33:24 --- quit: sts-q (Ping timeout: 260 seconds) 19:36:46 --- join: sts-q joined #forth 19:37:20 right 19:37:39 proving stack-based factorial correct should be a good early milestone, to at least see it works 19:37:53 hm, then I would need to read up on the mutable references section of PLF 19:38:00 to model ! and @ properly 19:39:55 yeah, I'm not gonna be any help there, lol; I've got a friend who does... something with separation logic, I've been meaning to get some stuff from him to read up on 19:42:11 oh yeah, sep logic would be cool 19:42:29 remexre: see also another good book: https://github.com/achlipala/frap 19:43:16 --- quit: LispSporks (Ping timeout: 245 seconds) 19:43:20 ooh, I'll put that on my list 19:43:21 thx 19:49:20 remexre: why would you need separation logic at first though 19:49:32 isn't that for like, reasoning with pointer-based structures? 19:49:44 or maybe it applies to everything involving memory, I forget 19:50:04 it's basically for things like 19:50:15 { #0 = 5 } +1 { #0 = 6 } 19:50:20 how do I know that #1 didn't change 19:50:40 oh you're doing stack in memory right 19:50:43 yeah 19:51:09 because that'd be a pretty easy thing to derive for me, where I just model the language with a stack initially 19:51:11 That all sounds interesting as hell. I wish I could follow it a bit better. 19:51:13 but I see 19:52:22 well, my point was more, I didn't write anything about #1, so I want to be sure it didn't change; hoare triples don't guarantee this by default (as I understand them at least) 19:52:43 oh right, in Hoare logic you really only make assertions about things you care about 19:53:00 so there might be a situation where #1 actually changes but you never checked, since you only asserted #0's value after +1 19:53:50 I just remembered yeah, when I showed { X = n } fib { X = fib n }, I completely discarded information about then intermediate variables Y and Z 19:54:15 KipIngram: yeah, logical foundations ( https://softwarefoundations.cis.upenn.edu/lf-current/index.html ) is the standard text for learning about some of this stuff :) 19:56:05 KipIngram: when we write { P } c { Q }, we mean that P and Q are assertions about the state, and that if P holds before running c, then Q holds after running c 20:02:15 --- join: LispSporks joined #forth 20:05:15 Cool - I will look that over. 20:05:42 BTW, I found another old calculator one of my kids used over the years. I don't know for sure it works - need to find some fresh batteries. 20:05:48 This one is a TI-84. 20:06:24 KipIngram: nice, I have a Forth for that!! 20:06:34 you need to try out my forth then :) 20:07:53 it's annoying that TI called it TI-84+ but there is no TI-84 model, hah 20:07:57 Oh, superb. 20:08:20 Yeah - I'd like to. I'll try to get the thing fired back up tomorrow. 20:08:35 KipIngram: latest release (as an .8xp file) here https://github.com/siraben/ti84-forth/releases/tag/1.1.0 20:10:11 Cool 20:16:06 --- quit: proteusguy (Remote host closed the connection) 20:23:32 --- quit: LispSporks (Ping timeout: 276 seconds) 20:26:18 --- quit: Zarutian_HTC (Ping timeout: 246 seconds) 20:33:04 --- quit: nihilazo (Quit: Gateway shutdown) 20:38:01 --- quit: proteus-guy (Ping timeout: 265 seconds) 20:42:05 KipIngram: just realized there's a hash mismatch between what I'm building and what the release says, it's probably because I finally stabilized the version of the assembler I was using heh 20:42:11 i'll do a minor bump then 20:45:19 I'm guessing I need to scruff up some sort of cable for it? 20:46:30 Yes, I forget what kind of cable it is but it's the port that is NOT the I/O port 20:46:35 so it looks like a printer cable 20:54:55 --- quit: lonjil (Quit: No Ping reply in 180 seconds.) 20:57:27 --- join: lonjil joined #forth 21:20:45 --- join: mtsd joined #forth 21:21:03 --- join: proteus-guy joined #forth 21:25:20 --- quit: mtsd (Ping timeout: 252 seconds) 22:16:45 --- join: Zarutian_HTC joined #forth 22:28:44 --- join: gravicappa joined #forth 22:38:14 --- join: spal joined #forth 22:44:20 --- join: andrei-n joined #forth 22:59:00 --- join: nihilazo joined #forth 23:59:59 --- log: ended forth/21.05.04