ComFreek

Bringing machine 'default' up with 'virtualbox' provider...
[default] Importing base box 'debian-wheezy72-x64-vbox43'...

[default] Matching MAC address for NAT networking...
[default] Setting the name of the VM...
[default] Clearing any previously set forwarded ports...
[default] Clearing any previously set network interfaces...
[default] Preparing network interfaces based on configuration...
[default] Forwarding ports...
[default] -- 22 => 2222 (adapter 1)

ComFreek

/**
 * This is a compilation of code snippets required to render SVG files in JavaFX using Batik.
 * See my full post on StackOverflow: http://stackoverflow.com/a/23894292/603003
 */

package proofofconcept;

import java.awt.image.BufferedImage;
import org.apache.batik.transcoder.TranscoderException;
import org.apache.batik.transcoder.TranscoderOutput;

ComFreek

Windows: Using SSH keys comfortably with Git, SVN, and remote servers

also works for Git Bash and Cygwin users on Windows

1. Be sure to have a recent version of Windows 10 (>= Windows 10 1809)

2. Activate Microsoft's official OpenSSH feature

3. Install

ComFreek

Typings for the @google/maps package

Forked from https://gist.github.com/lukas-zech-software/a7e4a23a6833ec1abb1fc836138f7822 (thanks to @lukas-zech-software!) and modified to include typings for the Directions API as well.

Hopefully, this will once be available officially from Google, see googlemaps/google-maps-services-js#42.

Usage

1. Install @google/maps if you haven't do so already: npm install @google/maps --save.

ComFreek

\documentclass[]{article}

% Make `:` behave as if you typed `\colon`.
% In particular, this allows you to concisely write `t: A` for a typing assertion while still
% getting the correct spacing of `\colon`.
%
% source: <https://chat.stackexchange.com/transcript/message/56900862#56900862>
% author: Skillmon <https://tex.stackexchange.com/users/117050/skillmon>
\begingroup
\lccode`\~=`\:

ComFreek

As a follow-up to today's discussion of HOAS, here is another example: https://en.wikipedia.org/wiki/Higher-order_abstract_syntax#Use_in_logical_frameworks

That example is based on Twelf, which for the purpose of that example, you can think of MMT. In fact, Twelf can be seen as a predecessor of MMT.

Apparently, there's also this classic paper by Pfenning and Elliott on HOAS. The paper's presentation might be a bit too far away from MMT for it to be easily understandable to you. But Section 2 ("motivating examples") might still be of interest to you: it mentions problems of substitution and variable occurrences, which you usually have if you're representing bound variables as mere "string references". I think you might be able to understand bits even if not all of the syntax. (Neither do I understand their syntax by mere glancing.)

By employing, HOAS we completely forego those problems by using meta-level functions (namely from LF). (Internally, these do work

ComFreek

Automatically save your WeeChat configuration and buffer list every day (24h have 86400000 milliseconds):

/trigger add autosave_config_timer timer 86400000;0;0 ""  "" "/mute /save"
/trigger add autosave_join_timer timer 86400000;0;0 ""  "" "/mute /autojoin --rune"
/trigger add autosave_layout_timer timer 86400000;0;0 ""  "" "/mute /layout store"

Upon an upgrade, restore:

ComFreek

Games by Natomic Studios (I like) + Downloads

• Natomic Studios: group of developers which published games created with Multimedia Fusion in early 2000s; they do have a "Natomic Studios" Facebook page
• The Daily Click: website collecting current and old games that are all done with Multimedia Fusion (?)

Note on running the games

• You might need a cnc232.dll -- a runtime library of Multimedia Fusion. Here's a version of cnc232.dll archived by The Wayback Machine. Put it into the same folder as the .exe of the game that interests you and that needs the library.
• Bananarama has a slow movement of the monkey character on Windows Vista and upwards. The game music is still fine, and it's still playable, prob

ComFreek

From Coq Require Import Init.Logic.

Axiom X: Type.
Axiom a b: X.

Axiom P: X -> Prop.
Axiom Q: P b -> Prop.

(*

ComFreek

POPL 2021: https://app.clowdr.org/conference/popl2021

• Mechanized Logical Relations for Termination-Insensitive Noninterference
• A practical mode system for recursive definitions
• λs: Computable semantics for differentiable programming with higher-order functions and datatypes
• On the Semantic Expressiveness of Recursive Types - very funny lightning talk