I bought M1 MacBook Air. It is the fastest computer I have, and I have been a GNOME/GNU/Linux user for long time. It is obvious conclusion that I need practical Linux desktop environment on Apple Silicon.
Fortunately, Linux already works on Apple Silicon/M1. But how practical is it?
I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.
Q: What is cubical type theory?
A: It’s a type theory giving homotopy type theory its computational meaning.
Q: What is homotopy type theory then?
A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.
| # Ubuntu 18.04 and various Docker images such as openjdk:9-jdk throw exceptions when | |
| # Java applications use SSL and HTTPS, because Java 9 changed a file format, if you | |
| # create that file from scratch, like Debian / Ubuntu do. | |
| # | |
| # Before applying, run your application with the Java command line parameter | |
| # java -Djavax.net.ssl.trustStorePassword=changeit ... | |
| # to verify that this workaround is relevant to your particular issue. | |
| # | |
| # The parameter by itself can be used as a workaround, as well. |
| benchmarking vec base | |
| time 15.54 μs (15.43 μs .. 15.63 μs) | |
| 1.000 R² (1.000 R² .. 1.000 R²) | |
| mean 15.45 μs (15.40 μs .. 15.51 μs) | |
| std dev 180.4 ns (157.0 ns .. 209.1 ns) | |
| benchmarking vec roman | |
| time 16.86 μs (16.77 μs .. 16.95 μs) | |
| 1.000 R² (1.000 R² .. 1.000 R²) | |
| mean 16.86 μs (16.81 μs .. 16.92 μs) |
| * { | |
| font-size: 12pt; | |
| font-family: monospace; | |
| font-weight: normal; | |
| font-style: normal; | |
| text-decoration: none; | |
| color: black; | |
| cursor: default; | |
| } |
This describes how I installed and configured my Raspberry Pi model B (512MB).
The Pi is mainly used as SSH jump host, IRC client, Git server, backup fileserver, etc. It doesn't need stellar performance, it just has to be cheap, low in power usage, and secure.
| # -*- coding: utf-8 -*- | |
| import os | |
| from flask import Flask | |
| from flask_heroku import Heroku | |
| from flask_sslify import SSLify | |
| from raven.contrib.flask import Sentry | |
| from flask.ext.celery import Celery |
| # | |
| # templatetags/kwacros.py - Support for macros in Django templates | |
| # | |
| # Based on snippet by | |
| # Author: Michal Ludvig <michal@logix.cz> | |
| # http://www.logix.cz/michal | |
| # | |
| # modified for args and kwargs by Skylar Saveland http://skyl.org | |
| # |
