| # COMMENTARY ON RETRO68 APPLICATION BUILD PROCESS | |
| # =============================================== | |
| # | |
| # About | |
| # ===== | |
| # Retro68, the cross-compiler toolchain for the classic 68k Macintosh (e.g. System 7), uses | |
| # cmake makefiles. I prefer to use standard makefiles. To reverse-engineer how Retro68 | |
| # builds a sample application with a custom resource file, I built the sample application | |
| # Samples/Dialog. | |
| # |
| <!-- We Timothy Robards' webcam filter codepen as a starting | |
| point for this webcam B or W conversion test. | |
| https://codepen.io/trobes/pen/bxropm | |
| --> | |
| <!-- | |
| PURPOSE: this is a Canvas-based prototype of a RGB-to-grayscale-to-dithered BandW | |
| conversion scheme that | |
| – can be done, per pixel, immediately after generating a source pixel colour; | |
| – uses storage at most equal to one graphics buffer, plus a comparatively small |
| Require Import Coq.Strings.String. | |
| Require Import Coq.Lists.List. | |
| (** * A taste of Curry-Howard | |
| In particular, how do we show a λ-calculus term is valid proof for a logical proposition? | |
| ** An overview | |
| To be more specific: I assume you've worked before with deduction systems that are given in the assumptions-over-conclusion notation. (If you've seen them stacked on top of each other in proof trees, so much the better.) In particular, if you understand a definition in that form of a relation like the has-type or evaluates-to relation, you should be set. |
| <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" | |
| "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> | |
| <html xmlns="http://www.w3.org/1999/xhtml"> | |
| <head> | |
| <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> | |
| <style type="text/css"> | |
| body { padding: 0px 0px; | |
| margin: 0px 0px; | |
| background-color: white } |
| "use strict"; | |
| /* | |
| tumblr-downloader.js - a Node.js script to download all media files posted in | |
| a Tumblr blog, most recent first. | |
| Usage: | |
| node tumblr-downloader.js | |
| Options - domain to download from, API key, and so on - are exposed below. |
or: How I printed and bound a 600 page book in less than one day
Dylan McNamee
This guide is a result of following Dylan McNamee’s own: it adds in missing details (stack trimming included), and covers a few hiccups to avoid. What is here wouldn’t have been possible without his guide.
What’s covered, and what isn’t
coqide-8.5pl1-ssreflect.7z - around 75 MB. (Smaller than the standard CoqIDE bundle!)
A great big caveat: the app bundle is no longer codesigned. If you wish to keep CoqIDE*.app codesigned, install a clean CoqIDE*.app, and replace the Resource/bin and Resources/lib/coq/user-contrib with the ones here.
I’m sure the reference manual is out of date - instead, I use test cases from the mathcomp/ssrtest folder. Note the new, extended library import paths. Try this, for example:
| > module Micro | |
| > import Data.String | |
| Another implementation of λ_Π | |
| ============================= | |
| An implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if | |
| - you have read "A tutorial implementation of a dependently typed lambda calculus", and now understand how to use a dependently-typed language, if not implement it; | |
| - you can write a Scheme metacircular interpreter; | |
| - understand how to write the usual suspects in an expressive type system like Idris'; |
| #!/usr/bin/env stack | |
| -- stack runghc --package text --package turtle | |
| {-# LANGUAGE OverloadedStrings #-} | |
| {- | |
| lxx2md.hs (-l|--lang LANG) | |
| A filter that converts Bird-style lhs in Markdown ``` blocks. | |
| Combines consecutive Bird-tracked lines into single blocks. |
module Micro
import Data.StringAn implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if