00:00:00 --- log: started forth/21.03.01 01:04:39 --- join: dave0 joined #forth 01:55:50 veltas: I looked into it a bit more and found the axiom you were referring to that's used at the foundational level for real analysis: https://en.wikipedia.org/wiki/Axiom_of_dependent_choice 01:57:03 Apparently AOC implies this but not vice versa, so it's weaker and rules out paradoxes like Banach-Tarski 01:58:33 I think the closest we got to this was when we used the well-ordering property of natural numbers to prove some things, didn't get to talking about moduli of Cauchy sequences though 01:58:43 Interesting nonetheless. 02:54:29 --- join: xek joined #forth 02:55:50 --- quit: APic (Ping timeout: 276 seconds) 03:13:27 --- join: APic joined #forth 03:35:18 --- join: hosewiejacke joined #forth 03:36:56 --- join: f-a joined #forth 03:50:50 --- quit: APic (Ping timeout: 245 seconds) 03:51:23 --- join: APic joined #forth 04:10:50 --- quit: hosewiejacke (Ping timeout: 245 seconds) 04:38:39 --- join: hosewiejacke joined #forth 05:06:32 --- quit: dave0 (Quit: dave's not here) 05:43:58 --- join: elioat joined #forth 05:57:05 --- quit: f-a (Ping timeout: 245 seconds) 06:42:26 --- join: f-a joined #forth 06:54:35 --- quit: hosewiejacke (Ping timeout: 245 seconds) 06:58:21 --- quit: Zarutian_HTC1 (Ping timeout: 245 seconds) 06:59:45 --- join: hosewiejacke joined #forth 07:16:51 --- join: tech_exorcist joined #forth 07:16:55 --- quit: shmorgle (Quit: [TalkSoup] via NEXTSPACE) 07:17:55 --- quit: tech_exorcist (Remote host closed the connection) 07:18:16 --- join: shmorgle joined #forth 07:20:00 --- join: tech_exorcist joined #forth 07:41:30 --- quit: f-a (Quit: leaving) 08:02:10 --- join: Zarutian_HTC joined #forth 08:17:07 mark4: Do tell us if you get through to CM about IRC 08:19:35 --- quit: hosewiejacke (Ping timeout: 245 seconds) 08:36:02 --- join: hosewiejacke joined #forth 08:46:15 --- quit: hosewiejacke (Ping timeout: 245 seconds) 08:46:45 --- join: f-a joined #forth 09:53:00 --- join: hosewiejacke joined #forth 10:04:10 --- quit: hosewiejacke (Ping timeout: 245 seconds) 10:16:06 --- join: hosewiejacke joined #forth 10:44:54 --- quit: ovf (Ping timeout: 260 seconds) 10:47:17 --- join: ovf joined #forth 10:58:09 siraben: https://math.stackexchange.com/a/489776 As you put in a more polite way, AOC has nothing to do with the definition of real numbers 10:58:19 To correct myself 11:00:39 I do know it applies to results in real analysis though 11:05:36 Yeah, I think those types of things would be deferred to a graduate course im analysis. 11:06:11 Pretty funny that even as you take the higher undergrad courses in math they're still introductory, because the theories are quite well developed 11:06:14 I think it's more interesting if you do axiomatic set theory, a good course on ZFC or similar will end with defining real numbers and some extremely basic analysis 11:06:48 I'm a big fan of constructivism and type theories like Calculus of Constructions 11:07:07 so yeah would be needed if I wanted to build analysis from scratch in Coq/Agda 11:07:09 Maths is an exercise in understanding complicated pure theoretical stuff, a maths degree is kind of like a very high brow IQ test :P 11:07:21 I suppose there is a lot of problem solving and rigour trained as well 11:08:04 introductory calculus was probably the worst of it because it's non-rigorous and lots of arbitrary things to memorize 11:08:26 Yeah my uni never did that 11:08:34 Are you doing maths or CS? 11:08:37 a constructivist 11:08:39 in forth 11:08:42 Sorry I'm sure you've told me this before 11:08:48 veltas: both! 11:08:54 "discrete maths"? 11:09:05 pure 11:09:17 Anyway, if you're doing maths courses, at my uni we never did "boring rote calculus" or anything like that, 11:09:33 that was like intro calc 1st year 11:09:44 Day 1 we were doing analysis 11:09:49 And set theory 11:10:00 heh nice, Europe I imagine 11:10:00 And algebra 11:10:03 Yes 11:10:31 north american curricula pale in comparison sometimes 11:10:39 that's great 11:10:52 There is no standard 'curriculum' in the UK 11:11:41 I know there's a lot of electronics folk here, I wonder if I should do some signal processing classes/Fourier analysis 11:11:46 Right 11:11:57 bbl 11:12:05 Signal processing is definitely worth knowing 11:12:37 As is fourier analysis, although the answer on whether to take those *classes* depends on your lecturers and individual course quality 11:12:44 You can learn all this stuff in your own time... 11:15:38 --- quit: Zarutian_HTC (Ping timeout: 240 seconds) 11:35:08 --- join: jai_cha joined #forth 11:36:16 hi, is there a forth bot here? 11:36:56 ciao jai_cha , I do not think os 11:36:58 *so 11:38:06 sad, my distro doesn't have a forth included 11:38:37 really? 11:38:40 not even gforth? 11:38:44 no 11:38:56 mhhh 11:39:01 which distro is that 11:39:06 alpine 11:39:41 edge/testing has it, if you feel like enabling that :p 11:39:53 gforth? 11:39:57 yeah 11:40:46 cool, although, my experience is that many packages never make it from testing to stable 11:41:01 I mean 11:41:09 compiling the tar.gz yourself is a way too 11:41:13 yeah... gnuware is probably especially tricky given musl doesn't try to implement all of glibc's... unique behaviors 11:41:16 it is supereasy, iirc just `make` 11:42:13 if I have to compile stuff I think I'm going for something else, gforth is not very much alive (dead?) 11:42:34 maybe retroforth 11:42:57 --- quit: gravicappa (Ping timeout: 240 seconds) 11:43:20 gforth is quite alive 11:43:30 but any forth will do 11:43:34 laters 11:43:38 --- quit: f-a (Quit: be back in a bit) 11:48:19 --- quit: Keshl_ (Ping timeout: 264 seconds) 11:48:20 do you use forth with alloc? Last time I tried forth I did not fear really comfortable manually managing memory. 11:48:46 personally I do, but I mainly use forth without an operating system 11:49:40 so I'm using a dictionary stored in a fixed buffer until I get a "normal" ALLOCATE/FREE allocator up and running 11:49:54 remexre: embedded development? what forth do you use? 11:50:16 OS development; my own :) 11:50:27 wow 11:50:34 https://git.sr.ht/~remexre/stahl/tree/main/item/kernel/src/common/forth 11:50:46 writing a forth is a relaly really good learning experience for forth, tbh 11:51:25 did you use that heavily commented x86 forth as a guide? I don't remember the author 11:52:33 I mostly used Moving Forth, A Beginner's Guide to Forth, and https://forth-standard.org/ 11:52:57 Moving Forth: http://www.bradrodriguez.com/papers/moving1.htm 11:53:06 A Beginner's Guide to Forth: http://galileo.phys.virginia.edu/classes/551.jvn.fall01/primer.htm 11:53:22 but this is like the 4th or 5th one I've written, so a lot of the "rough edges" have been "smoothed out" 11:54:19 the first one I wrote ( https://github.com/remexre/forth386 ) was fairly clumsy by comparison 11:55:38 remexre: is stahl for arm64 like raspberry pi 4? 11:56:11 yeah, though I care more about the rk3399 (as used in the rockpro64 and pinebook pro) than the pi (don't actually own one) 11:56:27 arm64 assembly is just _so much nicer_ to write than amd64 11:56:40 and not having to deal with acpi is a big plus 11:56:42 I'm on a rpi4 right now 11:56:50 I can try that, how do I compile it 11:58:14 it definitely won't boot there, arm boards in general need custom linker scripts, a bootloader, etc 11:58:32 but it's built using the Nix package manager, just run nix-build with it installed 11:58:47 right now it really won't run anywhere but qemu though 11:59:15 older revisions worked on the rk3399, but they didn't do interrupts right so most of it ended up getting scrapped 11:59:33 and I'm slowly making my way thru the ARM GIC docs... 12:00:55 I thought it could work with all arm64 boards without customization, but I see I was wrong 12:01:21 if you do wanna mess around with it under qemu, ./run.py starts it; at the moment, the easiest way to play around with things will be by dropping them in the 99-testing.fth file; there's an example of what a REPL would look like in src/platforms/js/90-repl.fth, but I need to finish interrupts to be able to do input 12:02:00 yeah, ARM stuff is way less standardized in general; there's some recently-released? spec for SBCs' boot process, but it's based on UEFI and therefore dumb (only half joking...) 12:02:16 and idk of anything that "natively" supports it (i.e. supports it in rom or something) 12:03:01 f I run it in qemu here I don't have any advantange compared to running it in x86 right? 12:04:30 not really; I keep KVM disabled because it's a bit funky on one of my boards 12:07:48 remexre: well, maybe I'll try when I'm back at my laptop then, thanks for the chat and the link, bye! 12:08:01 --- quit: jai_cha (Quit: leaving) 12:09:55 --- join: inode joined #forth 12:28:35 --- join: f-a joined #forth 12:45:43 does alpine forth run on an arm processor? 12:46:04 try github.com/mark4th/t4 12:46:13 thats an arm thumb2 sub threaded forth 12:46:57 already tested in on beagleboard black, beaglebone and every version of PI there is 12:53:17 mark4, I've been trying to use x4, but on every one of my machines it throws the following error: 12:53:19 Unknown TERM: /usr/share/terminfo/x/xterm-256color 12:53:44 I thought it was becasue of my weird virtualized setup on a chromebook, but I get it on straight debian, too 12:53:54 any ideas? 12:53:59 no worries if not, though 12:56:48 --- quit: jess (Quit: K-Lined) 12:57:55 --- join: jess joined #forth 12:58:57 aha 12:59:04 are you using debian? 12:59:21 i THOUGh i had that fixed, maybe you are using an older version 12:59:35 thats because debian puts the terminfo database in /lib/terminfo <--- DUMB 12:59:53 and i was ONLY looking in /usr/share/terminfo previously 12:59:56 add relevant terminfo 13:00:15 i.e. I have 13:00:16 f@extensa:/tmp$ tree ~/.terminfo/ 13:00:16 /home/f/.terminfo/ 13:00:16 └── s 13:00:16 └── screen-it -> /home/f/cfg/dot-files//tag-term/terminfo/s/screen-it 13:00:17 --- quit: lispmacs (Read error: Connection reset by peer) 13:00:19 1 directory, 1 file 13:01:01 here are 4 locations where a terminfo database can be. /etc/terminfo/ ~/.terminfo, lib/terminfo and /usr/share/terminfo. i was only looking in /usr/share 13:01:13 i now look in /lib/terminfo too i though 13:02:14 yeah, this is debian 13:02:17 buster 13:02:21 think the only valid reason for having ~/.terminfo in that list is if you are creating your own terminal 13:02:34 when did you last download from github? 13:02:43 i think i did that fix a few months ago now 13:02:43 this AM 13:02:51 err 13:02:55 and its still not working? 13:02:59 I'm on whatever the default branch is 13:04:46 does my shell matter, maybe? 13:05:00 yea erm. im 9999.99% positive i made that fix AND pushed it to github lol 13:05:10 but NONE of the copies of x4 or x64 i have here on this machine have that fix 13:05:12 ugh 13:05:26 i basically rewrote src/ext/erminal/term.f 13:05:32 hmmm 13:05:45 the last commit I see in gitlog is Jul 19, 2019 13:06:11 yea erm 13:06:20 the fix WAS done but only on X64 not on x4 13:06:21 right repo? https://github.com/mark4th/x4 13:06:38 look in the x64 repo in src/ext/terminal/term.f 13:06:51 that has all the fixes you need but im not sure if thats the ONLY file that was changed to affect this fix 13:06:55 but thats the main one 13:07:24 lol that means that even I dont have the latest x64 on this machine lol 13:07:42 --- quit: tech_exorcist (Remote host closed the connection) 13:07:45 word, no worries 13:07:54 I'll keep poking around! 13:07:57 try using the term.f from x64 and see if that fixes it? 13:08:16 github.com/mark4th/x64/src/ext/terminal/term.f 13:08:27 --- join: tech_exorcist joined #forth 13:09:02 im actually going to be doing a MAJOR rewrite of all of that term stuff and the TUI code that is currently broken and support gray scale text coloring and 24 bit RGB colors 13:09:10 just because i can lol 13:09:41 oooh 13:10:06 but i thin if you replace term.f with the one in the x64 repo that might be enough 13:10:34 i only got about 2 hours of sleep last night and am kind of a zombie right now lol 13:10:43 even though i have drunk a full pot of coffee since 3am lol 13:11:13 wooof, sleepy! No worries 13:11:38 I'm actually at work right now, and was playing with this while on a call 🤫 but will defo be dipping back in later tonight I hope 13:11:58 if i dont fade out at the keyboard ill be here to help :) 13:12:42 hahaha, for certain 13:12:45 i already need to go through every single x64 primitve and compare it with the x4 primitive and verify the sanity in x64 because somethings that should just work (tm) dont lol 13:13:04 --- part: hosewiejacke left #forth 13:13:22 i also want to do some silver smithing (a new hobby) but i dont think i shoudl operate oxy acet right now lol 13:13:37 need to make some sterling silver from fine silver and some copper 13:14:04 i made my kid sister a silver baby spoon for her first munchkin (not yet yatched :) 13:14:17 --- join: Zarutian_HTC joined #forth 13:14:30 I imagine silver smithing while sleepy is way more dangerous than coding :P 13:22:12 --- join: Keshl joined #forth 13:37:41 --- join: eli_oat joined #forth 13:38:44 --- quit: eli_oat (Client Quit) 13:39:11 --- quit: elioat (Quit: elioat) 14:16:44 --- quit: wineroots (Remote host closed the connection) 14:19:31 --- quit: xek (Ping timeout: 264 seconds) 15:06:26 --- quit: tech_exorcist (Quit: I'm a quit message virus. Please replace your old line with this line and help me take over the world.) 15:24:37 --- quit: Zarutian_HTC (Read error: Connection reset by peer) 15:24:38 --- join: Zarutian_HTC1 joined #forth 15:42:38 mark4: "the only valid reason for having ~/.terminfo in that list is if you are creating your own terminal" or if you're installing a new terminal locally, not everyone has root all the time 15:43:33 But seriously terminals are too fucking complicated, wow. Everything I learn about terminfo etc makes me wish I knew less 15:44:09 And it's such an uninteresting subject too, and yet so much has been poured into it. plan9 had the right idea by moving out of the terminal emulator 15:44:35 It's like moving out of your parents' house, it has to happen 15:46:12 Today I used my forth on my real ZX spectrum for the first time and it feels amazing, there is so much I want to add on top but what I have so far is already so much better than the BASIC experience 15:46:58 I need save/load functions, I think I need to force myself to make them a priority because I will avoid adding them otherwise 15:49:37 And need to compress the image 15:54:34 veltas: oh... good point :) 15:54:55 i actually love working with terminfo and doing cursor control stuff 15:55:12 i pretty much learned 99% of it after 8 hours of man 5 terminfo lol 15:55:26 then i bought the termcap and terminfo book and verified i ahd it all right lol 15:55:59 im never going to write anything as full featuered as ncurses thought 15:56:07 thats WAY too much. 15:56:39 what kind of images do you need to compress 15:58:09 By image I mean the program 15:58:17 --- quit: X-Scale (Ping timeout: 240 seconds) 15:58:27 --- join: X-Scale` joined #forth 15:59:01 --- nick: X-Scale` -> X-Scale 16:00:32 I think I will use something like LZ77 16:04:51 Terminal comms, X11 and the web can all die in a fire 16:08:06 i was working on dynamic huffman encoding with custom tweaks lol 16:08:29 but i bured out ahd till literally the last few days have done NO personal programming in months 16:08:48 bugt lz is good too 16:10:04 but 16:10:42 The reason I would use something like LZ77 is to save space, the decompression algorithm can be extremely short 16:10:50 yes 16:11:00 and no need for a 32 meg tree lol 16:11:39 And it can be implemented with CMOVE (or CMOVE>?) 16:12:26 And it will probably do a reasonable job compressing my code 16:12:28 i like compression algoritms in general, i even invented one of my own that compressed a 32k image down to 90 bytes 16:12:36 but its VERY specific, not generic 16:13:37 deflate is my favourite 16:13:57 It's not extremely complicated, it's very fast, it's very good at compressing 16:14:33 thats part of the zip algorithms right? 16:14:37 Yes 16:14:48 pity about phill katz tho :/ 16:14:48 It's secretly used everywhere, actually 16:15:00 lost a lawsuit, won the compression wars :) 16:15:03 then died 16:15:18 It's the most underrated compression format 16:15:27 It's what gzip uses too 16:15:32 yup 16:15:54 People keep converting .gz to .bz, but .bz is slower to download+extract even with relatively slow download speeds 16:16:07 And the compression improvements are minute 16:16:11 ark -> pkark -> pkzip 16:16:27 i tend to use xz now 16:16:41 gzip 4 life 16:16:42 i dont care about compression OR decompression speed 16:17:03 but gzip is still freeking awesome lol 16:17:40 I care about performance and simplicity, gzip is not too complicated, performs well in quality and timing. 16:18:08 It's pretty complicated but in the grand scheme of things it's not, and I could mostly explain it in an hour lecture 16:18:22 fast compression, fast decompression, GOOD compression... pick 2 :) 16:18:43 Pick all of them, gzip is that 16:19:16 --- join: dave0 joined #forth 16:24:00 its always a tradeoff 16:24:19 xz gives better compression but slower decompression 16:24:31 so i always compress my kernels with xz 16:24:42 but gzip is too ubiquitous not to use everywhere else lol 16:24:55 its like auto pilot takes over 16:25:00 but i do use bz2 too 16:25:30 tar -cJvf or tar -czvpf 16:25:48 if im remembering them right after only 2 hours of sleep in the last 24 hours 16:26:09 --- quit: f-a (Read error: Connection reset by peer) 16:26:35 --- quit: inode (Quit: ) 16:29:13 there is lzf which is very fast and lightweight but poor compression 16:30:06 lol im surprised anyone is even bothering with comprssion at all these days when you have 2847642947238 T of drive space and 28745624 T of ram lol 16:30:08 it is also much simpler than the heavier algos 16:30:16 --- join: f-a joined #forth 16:30:21 but im an embedded engineer by trade and at heart 16:30:35 --- quit: f-a (Client Quit) 16:30:48 i implemented static huffman and dynamic huffman 16:30:59 but the dynamic was in C and i was porting it to forth 16:31:06 there's always good old compress 16:31:08 i implemented some nifty tweaks to it too 16:31:36 forth! 16:37:07 mark4: it's sometimes still a win.. it takes xxx milliseconds to read the file and yyy milliseconds to uncompress it.. you can balance the equation to minimize the time :-) 16:38:40 ya. reading a small file and decompressing it can be faster than reading a large one 16:38:56 but still... i have some UBER hardware here lol 16:39:07 not me :-( 16:39:36 i would give you my desktop, its got 64 gigs of ram but its been unreliable since it had water dripped into it 16:39:46 lga2011 at 4.7 ghz and 64 gigs of ram 16:39:49 i reckon an 8086 forth would make an awesome boot monitor for the peecee 16:40:08 i have 4gig of ram :-) 16:40:28 this laptop has 16 gigs and one day for NO REASON it refused to boot anything at all 16:40:35 i mean not off the drives 16:40:43 not windows, not innux 16:41:36 booted to a live usb drive and copied off all the data and then spend 3 weeks trying to get a bootable install of ANYTHING 16:41:50 weird 16:41:56 did the bios shit itself? 16:42:34 so because i needed to work i bought a m-tech laptop. paid for the old version which was out of stock and got one with a 10th gen i7 when it came in stock with 32 gigs 16:42:46 then got this laptop working again and had NO problems since 16:43:04 this is just a cheapo (ish) asus rog laptop 16:43:22 the m-tech is a beast that i pretty much used for nothing except playing ARK survival evolved 16:44:03 my desktop wich is OLD by todays standards is stiill really good by todays standards 16:44:14 but even after replacing the moterhboard its not stable 16:44:42 need to buy a lga2011 cpu. the one i got originally is an extreme that i OCd to 4.7 ghz 16:44:55 which was pretty cool back then lol and is still no slouch 16:45:07 specially with 64 gigs of ram... 16:45:25 i used to do android AOSP builds from make clobber to complete in less than 20 minuts 16:46:03 romain guy at google who worked on the gui i think was jelous lol 16:46:21 i offered to give him a shell account with root on it back then. no questions asked 16:46:24 but he declined 16:46:59 i think its about 8 years old now and ive hardly used it at all :/ 16:59:21 --- quit: Keshl (Read error: Connection reset by peer) 17:00:05 --- nick: Zarutian_HTC1 -> Zarutian_HTC 17:01:42 --- join: MrMobius joined #forth 17:03:48 --- join: eli_oat joined #forth 17:04:23 --- quit: eli_oat (Client Quit) 17:17:26 --- join: Keshl joined #forth 17:19:44 --- join: wineroots joined #forth 17:40:48 --- quit: cartwright (Remote host closed the connection) 17:43:11 --- join: cartwright joined #forth 18:06:07 --- quit: dave0 (Quit: dave's not here) 18:25:13 --- join: boru` joined #forth 18:25:16 --- quit: boru (Disconnected by services) 18:25:18 --- nick: boru` -> boru 18:49:07 --- join: jedb__ joined #forth 18:51:46 --- quit: jedb_ (Ping timeout: 260 seconds) 19:03:11 --- join: X-Scale` joined #forth 19:05:25 --- quit: X-Scale (Ping timeout: 245 seconds) 19:05:26 --- nick: X-Scale` -> X-Scale 19:20:29 --- join: jedb_ joined #forth 19:20:34 --- quit: jedb__ (Read error: Connection reset by peer) 19:24:36 --- join: jedb joined #forth 19:25:15 --- quit: jedb_ (Ping timeout: 260 seconds) 19:28:58 --- quit: jedb (Ping timeout: 240 seconds) 19:54:26 --- quit: Zarutian_HTC (Read error: Connection reset by peer) 19:54:27 --- join: Zarutian_HTC1 joined #forth 20:05:25 --- quit: cartwright (Ping timeout: 268 seconds) 20:18:26 --- join: cartwright joined #forth 20:19:57 jai_cha: I think the heavily commented x86 forth you're referring to is jonesforth 20:20:16 --- join: gravicappa joined #forth 20:20:52 veltas: yeah, would depend on lecturers 20:40:58 oh, siraben, don't remember if I told you or not, but I'm reimplementing+extending the calculating-correct-compilers paper as a class project 20:41:34 my advisor ended up teaching a program-calculation seminar, so this fits pretty neatly into it 20:41:42 remexre: wonderful! I think it's a great paper 20:41:47 Yay 20:42:07 I'd be curious to read about the project once you're done with it. In what way are you extending it? 20:42:58 I'm gonna take it down "the rest of the way" to assembly and do inlining, const-propagation, and dead-code-elimination on the assembly 20:43:40 if I have time, some of the JIT tricks GraalVM does wrt not bothering to generate code for cold branches 20:44:58 --- quit: sts-q (Ping timeout: 240 seconds) 20:59:20 --- join: sts-q joined #forth 21:08:09 And those passes will be done in a calculational manner as well? 21:15:03 I think the assembly pass is just normal compilation; the point I'm going for is more "hey you can get graalvm at home in only a couple months of weekend work, using calculation" than "... using only calculation" /shrug 21:15:21 ig normal compilation-as-a-jit, but same deal 21:33:28 Right. 21:33:39 remexre: do you plan to mechanize the proofs in Coq? 21:35:07 not really; I was gonna do it in Prolog or Mercury for convenience. if my thm prover existed in a working state (rn it's once again in the state of "stupid problems encountered, deleted the whole thing, will rewrite in 3-6mo") I might consider doing it there, but it's not 21:38:38 I see. 21:39:45 yeah, not interesting enough for publication or anything, but hopefully interesting enough to keep using 21:42:36 --- quit: Keshl (Read error: Connection reset by peer) 21:45:08 --- join: Keshl joined #forth 21:50:22 --- join: hosewiejacke joined #forth 21:52:05 --- quit: Keshl (Read error: Connection reset by peer) 22:14:39 --- nick: KipIngram -> Guest36043 22:15:34 --- join: KipIngram joined #forth 22:15:34 --- mode: ChanServ set +v KipIngram 22:16:11 --- quit: Guest36043 (Ping timeout: 272 seconds) 22:16:17 --- quit: hosewiejacke (Remote host closed the connection) 23:35:29 --- join: hosewiejacke joined #forth 23:59:59 --- log: ended forth/21.03.01