No.1221
I'm really sorry about textboard.org but Bitdiddle said the stress tests were badly needed and kept encouraging me. I hope it's back up soon.
No.1222
>>1221It seems to have returned from death.
…
Why are you testing in production?
No.1226
Currently implementing truth tables for propositional logic in Python. I am aiming to make it general enough so that I can represent every possible table (not just AND, XOR and the usual) with any number of truth-values.
Fun fact: if you have V truth values, then the number of possible truth tables for a binary connective (a truth table with two inputs, basically) is: V ^ (V ^ 2).
This number gets very big very quickly:
V - V ^ (V ^ 2)
1 - 1
2 - 16
3 - 19683
4 - 4294967296 (4.3 billion)
5 - 298023223876953125 (298 quadrillion)
No.1227
>>1226>with any number of truth-valuesWhat are you going to use for not(not(x))?
No.1229
>>1227Aha. My impression is that NOT(NOT(p)) has the same truth value as p in most many-valued logics, especially those with a finite number of truth values. The Wikipedia article will give some examples:
https://en.wikipedia.org/wiki/Many-valued_logicThe program I'm writing won't be able to handle intuitionistic logic, where NOT(NOT(p)) =/= p, because intuitionistic logic does not use truth tables. At least, it doesn't use finite ones.
No.1231
I am giving Coq another go, this time using
Programs and Proofs:
https://ilyasergey.net/pnp/I expect to lose track of what is going on somewhere around the middle of the third chapter.
No.1232
>Coq
>Lego
>Isabelle
You forgot to add TypeScript.
No.1233
>>1232What do you mean? If this is a joke, I don't get it.
No.1234
>>1233It is. You'll get it when you're older.
No.1235
>>1231As expected, it was progressing a bit too fast for me. Before continuing on to chapter 4, I am reading this tutorial:
https://mdnahas.github.io/doc/nahas_tutorialI like that it uses only the most basic parts of Coq and explains them in terms of the Curry-Howard correspondence. It makes me want to write my own proof assistant!
No.1236
Is there a better way to repeatedly destruct a hypothesis so that it can be handled in one go like here?
Goal forall n, n = 0 \/ n = 1 \/ n = 2 \/ n = 3 -> n - 3 = 0.
intros n Cs.
destruct Cs as [C|Cs]; try destruct Cs as [C|Cs]; try destruct Cs as [C|C];
rewrite C;
reflexivity.
Qed.
I guess "repeat" would kind of work, except for the last one where the naming wouldn't match.
No.1238
>>1231I finished this. I liked it a lot, although the last chapter maybe progressed a bit too quickly, I ended skipping most of the exercises there. Maybe I will return to it someday.
Should I continue with Software Foundations or should I try The Little Prover before it?
No.1241
OK, it's back up.
>>1240>What are you working on, textboard engineering?Nothing so lofty. I'm just contributing in my small way to the SchemeBBS community by providing bugfixes.
No.1242
>>1238Wow I thought
The Little Schemer will be some quick enjoyable read, but it is quite laborious. It took me a while to figure out how to follow along with the code as the instructions are not very user-friendly. I use "J-Bob/step" for the actual proving and only copy it into the proper "J-Bob/define" once it is done. It is pretty fun though and I am looking forward to reading the actual implementation too. It is just a bit too manual after Coq, you have to type a lot!
No.1244
>>1242I finished it but I am not satisfied. It could have had more examples on the main techniques, like how to construct the totality claims and such. It did not feel like by the end I understood the main principles, if there were any.
No.1247
>>1246Nice little website, good job!
No.1249
The SchemeBBS "fossil repositories" link gives
https://fossil.textboard.org/502 Bad Gateway
nginx/1.18.0
Posting in the sandbox gives
https://textboard.org/sandbox/1error 502
bad gateway
Anyone else seeing this?
No.1250
>>1249Nice repeating digits. Yes, for me everything dynamic gives 502 error, even viewing individual posts like here:
https://textboard.org/sandbox/1/1 No.1257
Nothing, I'm slacking off.
No.1258
>>1220Fixing a PS One the only issues it has is the black & white screen and the CD didn't run but i got that fixed and now i'm trying to find some cheap PS1 games.
No.1259
>>1258How do you go about something like that? I never had such a device.
No.1260
Is anyone else getting NXDOMAIN for bunkerchan.xyz?
No.1262
>>1261Yep, it's back up, thanks. It seems the registration with ovh was renewed at 2020-09-10T11:44:55.0Z.
No.1263
>>1256>Do you know any good books for intermediate programmers? Or maybe even for experts?For what language Anon?
No.1265
>>1264I haven't read this one myself but try "Expert C Programming: Deep C Secrets" and SICP is recommended by some.
No.1266
>>1265I've actually read both already… SICP is an introductory textbook, it's really good but not for experts. Expert C Programming had some fun stories but it's mostly just a collection of war stories.
No.1267
>>1266Have you tried reading the source of some of the languages themselves? Surely that would help you to become proficient
No.1269
Has anyone else started getting
>Please turn JavaScript on and reload the page.
>DDoS protection by Cloudflare
for bunkerchan.xyz?
No.1270
>>1269https://bunkerchan.xyz/gulag/res/7295.html#7296 says they will take it down in a week, when they are not being bot-raided anymore.
My cloudflare blocker already went off on bunkerchan for a while.
They must have had this in place for some time.
No.1272
>>1271What are you working on?
No.1273
The cloudflare JS is back on bunkerchan.
>>1272Tempting Raven, from the looks of it.
No.1275
>>1274I know what you mean, fug
No.1277
Rate my run-length encoding functions in OCaml. Here's the most simple:
let rec rle l =
match l with
| [] -> []
| h::t ->
match rle t with
| (h', n)::t' when h' = h -> (h, n+1)::t'
| t' -> (h, 1)::t'
And a somewhat more involved:
let rle l =
let rec iter c n l =
match l with
| [] -> [(c, n)]
| h::t ->
if h = c then iter c (n+1) t else (c, n)::(iter h 1 t)
in match l with
| [] -> []
| h::t -> iter h 1 t
No.1278
>>1277>Rate my run-length encoding functionsThe first one is recursive in the obvious way, which is why it's "most simple". The second one still has a pending "(c, n)::" operation to perform after the "(iter h 1 t)" subcall, so unless OCaml rewrites this for you this is also recursive, despite the "iter" name. To get an iterative version with what are effectvely cons-style lists, you'll need to build a partial result in an accumulator and reverse the accumulator at the end, ensuring that the reversal operation is also iterative.
iter-is-still-recursive/10
No.1279
>>1278Sorry, hope you like this better:
let rle l =
let rec aux c n l =
match l with
| [] -> [(c, n)]
| h::t ->
if h = c then aux c (n+1) t else (c, n)::(aux h 1 t)
in match l with
| [] -> []
| h::t -> aux h 1 t
I don't like the full accumulator passing style because the extra reverse is often more costly than saving some returns to the stack.
No.1280
>>1279>I don't like the full accumulator passing style because the extra reverse is often more costly than saving some returns to the stack.The recursive version performs a linear pass on the input list going up the stack, and a linear pass for the result list coming down the stack. The iterative version performs a linear pass on the input list to build the accumulator, and a linear pass for the result list to reverse the accumulator. The reversal phase is the same size as coming down the stack, so unless there is some OCaml peculiarity that intervenes, your cost assertion is false. Furthermore on large and poorly rle-compressible input lists the recursive version dies by overflowing the stack, while the iterative version keeps working.
renamed-not fixed/10
No.1281
>>1280Yes, if the list is that large, there's not much else to do other than moving the call stack to the heap. But for shorter lists, pushing three values to the stack is cheaper than constructing an extra cons cell for each element of the result.
No.1282
>>1281Does OCaml offer some way to write a conditional that tests whether the recursive version would blow the stack if it were to be run?
No.1283
>>1282It does not. But I know, Big Data and Machine Learning is the hip thing now, so here's your industrial strength run-length encoding:
let rle l =
let rec aux c n a l =
match l with
| [] -> List.rev ((c,n)::a)
| h::t ->
if h = c && n < max_int then aux c (n+1) a t else aux h 1 ((c, n)::a) t
in match l with
| [] -> []
| h::t -> aux h 1 [] t
No.1285
Find songs by artist in bash
find_by_artist() {
find . -type f -print0 \
| xargs -0 exiftool -artist 2>/dev/null \
| awk -v RS='======== ' -v FS='\n' -v ORS='\0' \
'$2 ~ /'"${1}"'/ { print $1 }'
}
No.1286
>>1256Try writing a lexer. I'm not adept at making algorithms and this confused me. Try making something to recognize numbers, comments, strings, and a few key words from C. Just tokenize an input txt file.
No.1287
I wanted to try write a simple dependently typed program because I always just prove things but Coq can do this too. So here are the Fibonacci numbers. First, the specification of what it means for a number to be "Fibonacci", the proposition `fibonacci n m' says that the nth Fibonacci number is m:
Inductive fibonacci : nat -> nat -> Prop :=
| fib0 : fibonacci 0 0
| fib1 : fibonacci 1 1
| fibS n a b m (Ha : fibonacci n a) (Hb : fibonacci (S n) b) (Hm : a + b = m) : fibonacci (S (S n)) m.
This is straightforward, we know that the 0th number is 0 (fib0), the 1st is 1 (fib1), and the (n+2)th is m, if m is a + b where b is the (n+1)th number and a is the nth.
No.1288
>>1287Here is the program itself:
Definition fib n : { m | fibonacci n m } :=
let aux :=
fix f n :=
match n with
| 0 => (exist (fibonacci 0) 0 fib0, exist (fibonacci 1) 1 fib1)
| 1 => (exist (fibonacci 1) 1 fib1, exist (fibonacci 2) 1 (fibS 0 0 1 1 fib0 fib1 eq_refl))
| S (S n) =>
let (Xa, Xb) := f n in
let (a, Ha) := Xa in
let (b, Hb) := Xb in
let Hab := fibS n a b (a + b) Ha Hb eq_refl in
(exist (fibonacci (S (S n))) (a + b) Hab,
exist (fibonacci (S (S (S n)))) (b + (a + b))
(fibS (S n) b (a + b) (b + (a + b)) Hb Hab eq_refl))
end
in fst (aux n).
The first line says that fib takes an argument n, and produces such an m, that it is the nth Fibonacci number. (But only a single one and does not say anything about possible other such values.) `exist' is what builds the dependently typed value: its first argument is the property of the value, the second the value itself, and the third is the proof of the property holding for that value. The algorithm is a bit unusual because of Coq's type system. To keep the system logically sound, every algorithm must terminate. In many cases, Coq can automatically detect which argument is decreasing with each recursive call, but in case of the usual recursive definition of Fibonacci, it cannot. With a small trick it can, but that leads to another problem: it must also keep track of `n' to make sure that what it returns is indeed the `n'th number. For this reason both that and the usual iterative version, where it counts from zero up to n, fail type checking because Coq can't establish that the n going in the recursive call and the n coming back are the same.
No.1290
Does anyone else keep getting SERVFAIL on DNS requests for wizchan.org?
No.1295
>>1294What company would feel threatened by the FSF? They are pretty irrelevant.
No.1296
>>1289I'm doing exercise 3.2 right now, and it told me to
> First, make an arithmetic that defines only addition, negation, and subtraction of vectors over a base arithmetic of operations applicable to the coordinates of vectors. Applying any other operation to a vector should report an error.But if I make it throw an error with `(error "Unsupported vector operation:" operator)', it makes extend-arithmetic fail on zero?. If I return with #f instead of raising the error, it seems to work. I also had to register the `vector?' predicate.
I don't know if I am just not paying enough attention to the text or it really just throws you into deep water with the exercises.
No.1298
>>1220I just got into linux lately and I'm still learning basic bash commands lol. So I'm basically just working on being able to properly use a computer. Nothing big but feels good.
No.1299
>>1298That's pretty cool, bash can be really powerful. It's not perfect but it is damn useful.
No.1300
>>1295The GPL license is problematic for the corporate world. Pretty much all proprietary software depends on open source projects and GPL makes leeching off of open source software in proprietary projects difficult. Therefore any organized group that promotes FOSS is a threat. It's all about the money.
I don't know how organized the smear campaign against Stallman was. IMO most likely it was just useful fools who went after him.
No.1302
>>1301I'm done with the main track of exercises, it was pretty disappointing. It's just 8 exercises and all of them are pretty simple, you don't really need to use any interesting C++ features. There are extra exercises and some of them are pretty interesting, but it's hard to get feedback on those. I'm still doing some of them but C++ is a mess, there's just so much to keep in mind while writing it, I don't think I'll using it in my free time much.
No.1303
>>1300Stallman is his own worst enemy, but his autism made him more effective up until recently.
No.1304
Does kind.moe seem to be down for anyone else? I keep getting
>Index of /
>Apache/2.4.29 (Ubuntu) Server at kind.moe Port 443
No.1310
>>1309I don't use anon.cafe due to their captcha/bypass nonsense. Please post the following in
https://anon.cafe/kind/res/46.html
>>122>due to excessive CPU usageYou were already told on kind.moe in the thread with 45 replies about the
Date and
expires timestamps in captcha response headers. Furthermore, in scheduleHandler.js:expiredCaptcha you have:
function expiredCaptcha(immediate) {
if (immediate) {
checkExpiredCaptchas();
} else {
schedules.expiredCaptcha = setTimeout(function() {
checkExpiredCaptchas();
}, captchaExpiration * 1000 * 1);
}
}
Notice the
>captchaExpiration * 1000 * 1in setTimeout.
Never set captchaExpiration to 0.
Separately, from Readme.md:
>* `noReportCaptcha`(Boolean): disables the need for captcha when reporting. No.1311
>>1310Do you think it is the captcha expiration that causes the excess load? It does not make sense to me, since the client was waiting 256 seconds, does the server just make new captchas without the client side asking for one?
No.1312
>>1311>Do you think it is the captcha expiration that causes the excess load?It is merely one item to check off the list.
>It does not make sense to me>does the server just make new captchas without the client side asking for one?No. The scheduleHandler has an expiration rescanning loop in expiredCaptcha that runs on a timeout of
>captchaExpiration * 1000 * 1Notice that the callee, checkExpiredCaptchas, ends by handing off to expiredCaptcha again.
No.1314
>>1313Exciting! I wish I could Linux for the first time again lol
No.1315
>>1313unless youre getting a job on that field spend that time doing something productive for yourself
Trust me the gentoo rabbit hole its deep
No.1316
>>1315Well yeah, I had the great idea of trying it first time on my nearly 20y/o thinkpad. So compiling the kernel failed after 15hours and 40minutes and I have absolutely no idea what to do about it.
I still don't feel like it was for nothing.
I am about to get a job in this field, but is it really that deep? Everything I heared from Gentoo lately was something like
>Basically the optimization isn't worth it anymore because of fast computers / the compiling time makes it evenor:
>You're already using arch (actually artix) so there isn't that much anymore you're going to learn through getting into gentooI thought both were invalid arguments, but it's surprising to hear the opposite.
No.1317
Should I learn Rust? Is it really going to replace C and C++?
No.1318
https://www.php.net/manual/en/features.file-upload.errors.php>UPLOAD_ERR_INI_SIZE>Value: 1; The uploaded file exceeds the upload_max_filesize directive in php.iniwhen trying to post in
>>>/a/12file size: 2780883
examples of posts over 4MB:
>>1239 >>1241 >>1284 No.1319
>>1318Obscure technical searches lead me to underground chans. nice to know you all continue to exist. please keep allowing indexers to crawl you so this will happen in the future, thank you.
No.1321
Can we get an admin answer to
>>1318 ? Is it misconfiguration or has the file size limit been lowered?
No.1322
>>1321Filesize limit was lowered.
No.1325
>>1324Goodluck, what kind of project(s) did you have in mind?
No.1326
>>1325mostly making stupid applications. somethings for automating some TTRPG processes, and something like a program that place customizable virtual waifu assistants on your desktop (which I think exists already). The big goal is to learn how to white hat properly while doing small software projects to avoid psychosis. Also it's good programming practice.
No.1327
>>1326if you would like to make a study group on this board I would be amenable to joining and going through your textbooks
although I would request to see the titles you're going through first
No.1328
>>1327sure thing Anon, though, to create that study group board, I think I'd need to progress further with my studies than where I currently am (I started just as I wrote that post). The books I've got lined up for reading are:
>Compilers: Principles, Techniques, and Tools (The Dragon Book)>Computer Networking: A Top-Down Approach (6th Ed)>Computer Systems: A Programmer's Perspective>Crafting Interpreters>Designing Data-Intensive Applications: The Big Ideas Behind Reliable, Scalable, and Maintainable Systems>Mathematics for Computer Science (Eric Lehman)>Operating Systems: Three Easy Pieces>Structure and Interpretation of Computer Programs (2nd Ed)>The Algorithm Design ManualThe list isn't in any particular order, and the book I'm on right now is SICP
No.1329
>>1328Thanks for the comprehensive list. A good portion of them seem interesting.
Especially the lower level stuff.
I don't think I'll be following along with SICP.. Reading some CL stuff instead.
On Lisp in particular.
Here's a link for anyone interested in SICP though. The formatting is nice.
https://sarabander.github.io/sicp/If you get anything out of SICP, I would like to know. I'm just going to put it off for now.
Not convinced Scheme is the way forward
No.1330
>>1329>especially the lower level stuffI should've mentioned I'm starting from near zero here. Besides some codemonkey experience in Python, C, and Lua.
>If you get anything out of SICP, I would like to know.I'll keep you posted Anon!
No.1331
>>1329SICP is not about Scheme, it doesn't even cover the full language. You will learn a lot from it even if you never use Scheme ever again.
No.1332
>>1331I skimmed the book further due to your suggestion. For a good hour or so.
It covers a lot of interesting computer concepts, most I am familiar with due to previous compsci books and lisp books.
https://en.wikipedia.org/wiki/Structure_and_Interpretation_of_Computer_Programs>It was formerly used as the textbook for MIT's introductory course in electrical engineering and computer scienceSo it doesn't seem practical to me, but it is a great introduction. Would definitely be practical for others.
I've never took the time to go through the ToC and jump around the chapters to make this conclusion before.
It would've been nice to have this as my introduction to computation, but oh well.
No.1333
>>1332I'll consider myself lucky to have it as my introduction then!
No.1334
Is textboard.org down?
No.1336
>>1335Thanks. Now it's back for me too, just super slow.
No.1337
Is anyone else getting captchas when trying to search for anything on:
https://archive.ph/ No.1338
>>1337That site sometimes turns on the captcha. web.archive.org doesn't require captchas but to archive a site, you need to enable JabbaShit.
No.1340
>>1338> That site sometimes turns on the captchaOK. It's been in this unusable state for me for a month and a half now.
> web.archive.org doesn't require captchas but to archive a site, you need to enable JabbaShit.Unfortunately it seems to require JS for searching as well. The only non-JS function seems to be serving archived pages if you have a direct link, but the direct link contains the archival timestamp, so it cannot be constructed from the target URL alone.
> The Wayback Machine requires your browser to support JavaScript, please email info@archive.org if you have any questions about this. No.1341
>>1340If I write some random number like 23 instead of the timestamp, I get the latest.
No.1343
>>1342They have an API, if you don't mind JSON you can use that:
https://archive.org/help/wayback_api.php No.2069
Is anyone else getting
> error 502
> bad gateway
when trying to post on textboard.org, including on /sandbox/?
No.2070
>>2069Yes I am getting the same error.
No.2280
I'm hacking with Emacs sliced images, i want to allow a better rendering of images and text, where text and images freely can be mixed, placed next to each other in horizontal, images in Emacs are fontified text, where the height of the image would be the height of the line, only one line of text can be placed horizontally to the image and is always centered. I have currently read most source code in Emacs relating to images, positioning and have studied packages which use sliced images. And have implemented basic functions for sliced image insertion which handles the correct scaling, slicing and properties to allow images to be represented as a block of text, which the image is scaled, resized and sliced to fit. I have mostly automatized everything and added different insertion methods which react correctly to the surroundings, such as a coordinate (absolute positioning) based insertion allowing HTML like manipulation of text and images.
If anyone is interested in my project; send me a message 3nity(at)airmail.cc
No.2288
>>1253Thanks for mentioning Logical Foundations. I looked it up and found a website that has various other related books to download
https://softwarefoundations.cis.upenn.edu/I rarely have time, but this goes on my list of stuff to read when the world slows down, I get independently wealthy, and my IQ increases.