Someone SomeoneSerge

Упражнения по формальным доказательствам

Нет времени объяснять, переходим сразу к делу.

Инструменты

Доказывать теоремы мы будем, используя интерактивные пруверы Isabelle или Lean 3. Примеры приводятся для каждого прувера, для решения задач же можно использовать любой из них.

Introductions and general info

Helper libraries

I've commented a few times about some issues I see with the scalability of ActivityPub - the protocol behind the Fediverse and its best-known implementation Mastodon. A couple of folks have asked for more elaboration, so ... here it is.

First, let me add some disclaimers and warnings. I haven't devoted a lot of time to looking at ActivityPub, so there might be some things I've misunderstood about it. On the other hand, I've brought bigger systems - similar node counts and orders of magnitude more activity per node - from broken to working well based on less study of the protocols involved. So if you want to correct particular misconceptions, that's great. Thank you in advance. If you want to turn this into an appeal to authority and say that I'm wrong only because I haven't developed a full ActivityPub implementation or worked on it for X years ... GTFO.

What

What is ActivityPub? It's an HTTP- and JSON-based protocol for exchanging information about "activities". An activity could be many things.

Context

I was helping a few computer science students and enthusiasts understand “how” modern processors got to be “so fast” outside of clock speed increases.

Here is the main ;p exert

Acronyms:

SIMD: Single Instruction, Multiple Data

Ran on /tmp (with useTmpfs), where the files are, and directly from TTY1 (without any DE running).

Shell A: nix shell nixpkgs#hyperfine nixpkgs#ffmpeg-headless
Shell B: nix shell nixpkgs#hyperfine chaotic#pkgsx86_64_v3.ffmpeg-headless
Benchmark parameter: hyperfine -w 3 -M 10
Benchmark command: ffmpeg -threads 1 -y -i 01._Radio_Ga_Ga.flac -f ogg /dev/null

	// Copyright (c) 2021 Francesco Mazzoli <[email protected]>
	//
	// Permission to use, copy, modify, and distribute this software for any
	// purpose with or without fee is hereby granted, provided that the above
	// copyright notice and this permission notice appear in all copies.
	//
	// THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
	// WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
	// MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
	// ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES

	#!/usr/bin/env python3
	from pathlib import Path
	from typing import Union, Tuple, List, NamedTuple, Dict
	import sys


	class Block(NamedTuple):
	name: str
	created: int
	updated: int

	/*
	minimod: A stripped down module system

	TODO Comparison:
	- [ ] Come up with a benchmark "logic" using plain old functions and let bindings
	- [ ] Write the benchmark for the module system
	- [ ] Write the benchmark for POP?
	- [ ] Qualitative comparison of extensibility in the context of composable
	Nixpkgs packaging logic
	TODO Fine-tuning:



	echo ""
	echo "********** Github Dork Links (must be logged in) *****************"
	echo ""
	echo " password"
	echo "https://github.com/search?q="hackertarget.site"+password&type=Code"
	echo "https://github.com/search?q=""hackertarget""+password&type=Code"
	echo ""
	echo " npmrc _auth"