[ a / b / cf / cy / g / lain ] [ fresh / meta ] [ home / rules / faq / affiliates ]

/g/ - Technology

Programming and Electronics
Name
Subject
Comment
File
Embed
Password (For file deletion.)

Hop in to our IRC channel! #wirechan@rizon.net

File: 1581460038602.png (503.48 KB, 934x1000, daily_programming.png)

 No.211

What are you working on, /g/?

 No.216

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.217

File: 1582269064422.jpg (160.42 KB, 800x998, marika_kato__bodacious_spa….jpg)

>>216
It seems to have returned from death.



Why are you testing in production?

 No.218

File: 1582283674971.jpeg (168.42 KB, 1000x1358, 4798701.jpeg)

>>217
>Why are you testing in production?
Setting up a local copy is such a hassle and Bitdiddle said:

>Don't worry about that. I'm sincerely grateful you found that severe bug, took the time to read the code and offered a way to fix the issue


>We badly need those. Now is the time.


>Thank you again for discovering that awful bug. I believe your stress tests will hit the nginx cache, so they should be safe.

 No.230

File: 1583269287742.png (1.42 MB, 900x1200, 1567550669432.png)

I am trying to change a pretty fundamental type in a functional program, as the current one turned out to be inadequate… Hopefully I won't end up having to rewrite the whole thing. How do functional programmers deal with cases like this? Just get it right before beginning?

 No.232

File: 1583344027901.jpg (38.38 KB, 249x332, capable.jpg)

>>230
Looks like I managed to avoid the situation. Though I am still curious how people deal with situations like that.

 No.257

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.258

>>257
>with any number of truth-values
What are you going to use for not(not(x))?

 No.260

File: 1586901531346.jpg (7.52 KB, 183x275, Curious Miku.jpg)

>>230
What exactly were you trying to do?

 No.261

>>258
Aha. 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_logic

The 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.262

File: 1586975322394.jpg (733.39 KB, 1000x1300, 7cabe45a4f8164a082f778b9b5….jpg)

>>260
It was an interpreter-like program where certain escape sequences were handled on the parsing side, but I needed to preserve them for later use. I ended up encoding them in the AST using already existing constructs but it's ugly and the proper way would be to change the AST. I know that the whole thing sounds horrible but believe me, it is actually much worse.

 No.286

File: 1589832842137.png (2.01 MB, 620x850, Generaltan.png)

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.287

>Coq
>Lego
>Isabelle
You forgot to add TypeScript.

 No.291

>>287
What do you mean? If this is a joke, I don't get it.

 No.292

>>291
It is. You'll get it when you're older.

 No.302

File: 1590733791715.jpg (1006.46 KB, 1214x1805, 5389b33aa21c88bc7304f934cc….jpg)

>>286
As 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_tutorial

I 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.315

File: 1591127549558.jpg (311.75 KB, 2400x3200, 59f557afe19fe20741c3e75c9c….jpg)

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.317

File: 1591988277700.png (337.88 KB, 792x720, 1450102382233.png)

>>286
I am really glad I started reading this, Coq is lots of fun.

 No.321

File: 1593463036175.jpg (614.33 KB, 1200x1680, 44ac5083e0a37d3fede1a06570….jpg)

>>286
I 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.322

File: 1593682205757.jpg (4.25 MB, 2254x3200, badgateway.jpg)

Can anyone post on textboard.org? I have a bug report and fix to post and I keep getting 502.

 No.323

File: 1593703931946.jpg (1.4 MB, 1103x1826, 15e8f3fbb248eb1faf2bec4f47….jpg)

>>322
I get 502 too… maybe you could post here instead? What are you working on, textboard engineering?

 No.324

File: 1593720787662.jpg (4.14 MB, 2244x3706, image.jpg)

OK, it's back up.

>>323
>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.325

File: 1594070761376-0.jpg (163.12 KB, 661x920, 1588027855042-prover.jpg)

File: 1594070761376-1.jpg (162.44 KB, 661x920, 1588027855042-sicp.jpg)

>>321
Wow 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.326

File: 1594320697293-0.gif (706.24 KB, 1280x1086, 90401bed27c927690db68bf6ee….gif)

File: 1594320697293-1.png (7.02 KB, 734x25, Screenshot_2020-07-09_20-4….png)

I'm hacking on some Scheme code and noticed this… Thank you Geiser, very useful info.

 No.328

>>325
I 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.329

File: 1594568499786.png (165.13 KB, 510x346, Nichtskapiert.png)

>>328
Actually, thinking about it a bit more, I think I get it now.

 No.330

>>211
On my personal website.
>https://kamel.surge.sh

 No.331

>>330
Nice little website, good job!

 No.332

>>331
Thanks :D

 No.333

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/1
error 502
bad gateway

Anyone else seeing this?

 No.334

>>333
Nice repeating digits. Yes, for me everything dynamic gives 502 error, even viewing individual posts like here: https://textboard.org/sandbox/1/1

 No.335

File: 1595113198153.jpg (658.87 KB, 900x1273, t.jpg)

>>334
Thanks for the confirmation. Hope it's back up soon.

 No.336


 No.343

File: 1595789829717.png (444.99 KB, 1280x720, 1595728207571-sicp.png)

I started reading the first volume of Software Foundations, Logical Foundations. It's pretty nice so far, but today I did nothing but the pumping exercise in the IndProp chapter and I still did not manage to finish it. I just can't figure out the App case. I already did every other case but this one just seems impossible.

Maybe I should be working on some project instead of always just reading.

 No.346

File: 1596142644191.png (10.36 KB, 855x855, 0b447a826e8900385d59db99a4….png)

>>343
I get too engrossed and spend all night playing with my Coq. This can't be healthy! I managed to figure out the pumping lemma but now I am stuck on palindrome_converse and can't progress at all. I need induction on (l = rev l) but of course the usual list induction won't do it, because (h :: t = rev h :: t) does not mean (t = rev t).

 No.349

File: 1596573228860.png (185.08 KB, 600x600, cc02bcb0378c60a175e8483b85….png)

>>343
>>346
I'm proud to announce that I have finished that chapter. If I continue progressing at this rate I might finish the first volume by the end of the year!

 No.357

File: 1597521488663.jpg (3.02 MB, 2168x1540, ceb7f68aee01f05954efeebd91….jpg)

I feel like I plateaued in my programming skills and have no idea where to go from here. I don't think learning the basics of yet another programming language would do much for me. Maybe I should start digging deeper into the things I already know, but it seems to be much harder than beginning things. It's hard to find book that are not aimed at beginners. Do you know any good books for intermediate programmers? Or maybe even for experts?

 No.373

Nothing, I'm slacking off.

 No.374

>>211
Fixing 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.375

>>374
How do you go about something like that? I never had such a device.

 No.380

Is anyone else getting NXDOMAIN for bunkerchan.xyz?

 No.381

>>380
It works for me.

 No.383

>>381
Yep, it's back up, thanks. It seems the registration with ovh was renewed at 2020-09-10T11:44:55.0Z.

 No.384

>>357
>Do you know any good books for intermediate programmers? Or maybe even for experts?
For what language Anon?

 No.385

File: 1599945380148.jpg (829.83 KB, 855x1200, 5756ac83809e1f39e91f10dffe….jpg)

>>384
Programming in general would be the best, but I would be interested in advanced books on C, bash, Python, Scheme, OCaml or Smalltalk too. At the moment I am basically interested in what separates the novice from the expert, is it just experience or could I somehow "accelerate" it by studying?

 No.386

>>385
I haven't read this one myself but try "Expert C Programming: Deep C Secrets" and SICP is recommended by some.

 No.387

>>386
I'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.388

>>387
Have you tried reading the source of some of the languages themselves? Surely that would help you to become proficient

 No.391

File: 1600110395748.png (128.59 KB, 457x645, thumbs_up.png)

>>388
That's actually not a bad idea. In university I worked on the frontend of a C compiler for a while and I learned a lot from it. Thanks!

 No.402

Has anyone else started getting
>Please turn JavaScript on and reload the page.
>DDoS protection by Cloudflare
for bunkerchan.xyz?

 No.403

>>402
https://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.404

File: 1601647372212.jpg (511.78 KB, 950x1343, 499bdca0d75e7fca0093367fec….jpg)

>>403
Thanks for the information. The JS barrier is once again down right now so I can see that they've added in-thread captchas, where previously they were only a barrier to creating new threads. Do you happen to know whether these newly added in-thread captchas will be reverted as well or is bunkerchan a captcha-only site from now on?

 No.405

>>404
What are you working on?

 No.407

The cloudflare JS is back on bunkerchan.

>>405
Tempting Raven, from the looks of it.

 No.459

File: 1608072096637.png (727.83 KB, 960x776, ece6c06fcbdb9dd0c7c4793cbd….png)

> tfw you want to go to sleep but you feel that you have *almost* solved that nasty problem
Sleep deprivation, here I come!

 No.460

>>459
I know what you mean, fug

 No.461

>>315

Goal forall n, n = 0 \/ n = 1 \/ n = 2 \/ n = 3 -> n - 3 = 0.
intros n Cs.
decompose [or] Cs; subst; reflexivity.
Qed.

 No.540

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.541

>>540
>Rate my run-length encoding functions
The 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.542

>>541
Sorry, 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.543

>>542
>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.544

>>543
Yes, 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.548

>>544
Does 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.550

>>548
It 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.551

File: 1612907484109.jpg (4.16 MB, 2266x3173, rias2.jpg)

>>550
fixed/10

 No.572

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.578

>>357
Try 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.581

File: 1614371873438.png (17.35 KB, 800x500, 87617512_p0.png)

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.582

File: 1614371892504.png (17.88 KB, 800x500, 87617512_p1.png)

>>581
Here 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.610

File: 1616484769382.jpg (68.13 KB, 550x814, cover.jpg)

Anyone else reading SICP2.0? My Scheme skills are a bit rusty but I am really happy to have an excuse to use it again.

 No.613

Does anyone else keep getting SERVFAIL on DNS requests for wizchan.org?

 No.614

File: 1617554820348.png (26.86 KB, 720x313, screenshot.png)

>>613
>wizchan
idk cause i don't post there but saw this on another board the other day

 No.615

>>614
Thanks.

 No.618

File: 1617913672356.png (122.3 KB, 529x482, richard_stallman.png)


 No.619

File: 1618001205173.png (302.39 KB, 1002x405, leah-rowe-defends-stallman.png)

>>618
>at the behest of proprietary software vendors
good to see no one's being paranoid about this whole thing

 No.620

>>619
What company would feel threatened by the FSF? They are pretty irrelevant.

 No.631

File: 1618346622484.jpg (171.17 KB, 1280x720, dumb.jpg)

>>610
I'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.



[Return][Go to top] [Catalog] [Post a Reply]
Delete Post [ ]
[ a / b / cf / cy / g / lain ] [ fresh / meta ] [ home / rules / faq / affiliates ]