Skip to content

Instantly share code, notes, and snippets.

Avatar
💭
GAAAA!!!

Shachar Itzhaky corwin-of-amber

💭
GAAAA!!!
View GitHub Profile
View playful-jscoq.html
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<script src="./node_modules/jscoq/ui-js/jscoq-loader.js" type="text/javascript"></script>
</head>
<body>
<script type="text/javascript">
class Observer {
View Dune log with -custom
Workspace root: /Users/corwin/var/tut/dune
Running[0]: /usr/bin/getconf _NPROCESSORS_ONLN > /var/folders/tz/ywq0c4d920n6lkpsgyggj25m0000gn/T/dune72a639.output 2> /dev/null
Auto-detected concurrency: 4
disable binary cache
Running[1]: /opt/local/bin/opam --version --color=never > /var/folders/tz/ywq0c4d920n6lkpsgyggj25m0000gn/T/dunee9b97a.output
Running[2]: /opt/local/bin/opam config env --switch default --sexp --set-switch > /var/folders/tz/ywq0c4d920n6lkpsgyggj25m0000gn/T/dune1af7ea.output
Running[3]: /opt/local/bin/ocamlc.opt -config > /var/folders/tz/ywq0c4d920n6lkpsgyggj25m0000gn/T/dunea3aa3c.output
Dune context:
{ name = "default"
; kind = { root = None; switch = "default" }
@corwin-of-amber
corwin-of-amber / 01-sll_init.sy
Created Nov 11, 2019
SuSLik pure synthesis mini-benchmarks
View 01-sll_init.sy
; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic UF)
(declare-var x Int)
(declare-var v Int)
(synth-fun target ((x Int) (v Int)) Int
((Start Int (0 1 x v))))
@corwin-of-amber
corwin-of-amber / Coroutines
Last active Oct 21, 2019
A utility library for coroutines in Emscripten (using Asyncify)
View Coroutines
emcc example.c -s ASYNCIFY \
-s ASYNCIFY_IMPORTS='["emscripten_sleep","emscripten_yield","emscripten_coroutine_create","emscripten_coroutine_next"]' \
--js-library library_coroutine.js
@corwin-of-amber
corwin-of-amber / firepad-nulladapter.js
Created Aug 9, 2019
A minimal "null-modem" Firepad adapter
View firepad-nulladapter.js
const {EntityManager, RichTextCodeMirror, EditorClient, FirebaseAdapter, utils,
RichTextCodeMirrorAdapter} = Firepad.firepad;
var upstream = [];
class NullAdapter {
constructor(userId, userColor) {
this.userId_ = userId;
this.color_ = userColor;
}
@corwin-of-amber
corwin-of-amber / log.txt
Last active Jul 14, 2019
simple-peer (trickle=false)
View log.txt
[Log] peer1->peer2 signal {"type":"offer","sdp":"v=0\r\no=- 3624713161162515430 2 IN IP4 127.0.0.1\r\ns=-\r\nt=0 0\r\na=group:BUNDLE 0\r\na=msid-semantic: WMS\r\nm=application 55189 DTLS/SCTP 5000\r\nc=IN IP4 79.176.64.37\r\na=candidate:842163049 1 udp 1677729535 79.176.64.37 55189 typ srflx raddr 0.0.0.0 rport 0 generation 0 network-cost 999\r\na=ice-ufrag:miMp\r\na=ice-pwd:cNw7qh/6H8O7UmZugyAKIshU\r\na=fingerprint:sha-256 53:F3:53:F6:AB:60:C1:6A:CC:0A:A9:98:48:4F:8A:62:0E:46:83:B0:39:C5:09:8F:6E:94:C6:A7:8F:32:04:90\r\na=setup:actpass\r\na=mid:0\r\na=sctpmap:5000 webrtc-datachannel 1024\r\n"} (peer-sanity.bundle.js, line 4773)
[Log] peer2->peer1 signal {"type":"answer","sdp":"v=0\r\no=- 7710368483432959926 2 IN IP4 127.0.0.1\r\ns=-\r\nt=0 0\r\na=group:BUNDLE 0\r\na=msid-semantic: WMS\r\nm=application 57305 DTLS/SCTP 5000\r\nc=IN IP4 79.176.64.37\r\nb=AS:30\r\na=candidate:842163049 1 udp 1677729535 79.176.64.37 57305 typ srflx raddr 0.0.0.0 rport 0 generation 0 network-cost 999\r\na=ice-ufrag:PF1b\r\na=ice-p
@corwin-of-amber
corwin-of-amber / log.txt
Last active Jul 14, 2019
simple-peer (trickle=true)
View log.txt
[Log] peer1->peer2 signal {"type":"offer","sdp":"v=0\r\no=- 5938417958810222947 2 IN IP4 127.0.0.1\r\ns=-\r\nt=0 0\r\na=group:BUNDLE 0\r\na=msid-semantic: WMS\r\nm=application 9 DTLS/SCTP 5000\r\nc=IN IP4 0.0.0.0\r\na=ice-ufrag:DZ9A\r\na=ice-pwd:mrnI5/tUWvqwS7garG8OYRZJ\r\na=ice-options:trickle\r\na=fingerprint:sha-256 F6:50:91:7B:C2:94:A3:35:7C:CC:1D:F3:A3:A7:B8:1D:E5:57:6E:C2:4E:B6:E4:B1:4F:F1:A9:C3:F1:F0:0B:2D\r\na=setup:actpass\r\na=mid:0\r\na=sctpmap:5000 webrtc-datachannel 1024\r\n"} (peer-sanity.bundle.js, line 4773)
[Log] peer2->peer1 signal {"type":"answer","sdp":"v=0\r\no=- 1864940161042314649 2 IN IP4 127.0.0.1\r\ns=-\r\nt=0 0\r\na=group:BUNDLE 0\r\na=msid-semantic: WMS\r\nm=application 9 DTLS/SCTP 5000\r\nc=IN IP4 0.0.0.0\r\nb=AS:30\r\na=ice-ufrag:BWgd\r\na=ice-pwd:QC44hjljq5cOku5ulbWRs5sF\r\na=ice-options:trickle\r\na=fingerprint:sha-256 20:BC:2A:36:E7:1C:17:A7:C3:62:21:96:37:5E:C5:34:D4:F9:9D:66:7A:74:EB:23:CE:9C:DA:3A:8D:0B:FB:39\r\na=setup:active\r\na=mid:0\r\na=sctpmap:5000 webrtc-datachannel
View git-remove-from-history
# Based on:
# https://confluence.atlassian.com/bitbucket/reduce-repository-size-321848262.html
for m in "$@" ; do # jscoq/coq-pkgs/*.coq-pkg ; do
git filter-branch --index-filter "git rm --cached --ignore-unmatch $m" HEAD
git for-each-ref --format="%(refname)" refs/original/ | xargs -n 1 git update-ref -d
done
# Prune all of the reflog references from now on back (unless you're explicitly only operating on one branch).
git reflog expire --expire=now --all
@corwin-of-amber
corwin-of-amber / marshal32.js
Last active Mar 15, 2019
Override js_of_ocaml's Marshal functionality with 32-bit truncation
View marshal32.js
/**
* This is a hack to circumvent a discrepancy arising when Coq is compiled
* as a 64-bit library and then passed through js_of_ocaml, resulting in
* 32-bit JavaScript code.
* As a whole, the Coq codebase makes little use of integer arithmetic and
* does not create huge arrays of more than 2^31-1 elements. An exception
* to this is hash values calculated for storing various Coq types in maps
* and hash tables and to speed up comparisons.
* Though the values themselves are meaningless, they are unfortunately
* stored in .vo files through use of the Marshal module, and lead to files
View LeaveMeAlone.user.js
// ==UserScript==
// @name LeaveMeAlone
// @namespace corwin.amber
// @description Prevents the leave confirmation dialog
// @include http://*.shinezone.com/*
// @version 1
// @grant none
// ==/UserScript==
console.log("Leave me!");