bookshelf

A study of the books listed below.

Overview

Most proofs are conducted in LaTeX. Where feasible, theorems are also formally proven in Lean.

• Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
• Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
• Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015.
• Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009.
• Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.
• Enderton, Herbert B. Elements of Set Theory. New York: Academic Press, 1977.
• Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
• Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.
• Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.
• Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.

Building

Nix

direnv can be used to launch a dev shell upon entering this directory (refer to .envrc). Otherwise run via:

$ nix develop

Container

Build and run the container like so:

$ podman build -t bookshelf .
$ podman run -p 4001:4001 bookshelf

You can also install the bookshelf.container Quadlet:

$ podman build -t bookshelf .
$ podman quadlet install bookshelf.container

Lake

If you prefer, you can also use the elan package manager like normal. Build the project by running

$ lake build
$ lake build Bookshelf:docs

View the generated files by running python3 -m http.server from within the .lake/build/doc directory.

NGINX

Use Let's Encrypt to get a TLS certificate:

$ certbot certonly --standalone -d bookshelf.jrpotter.com

You can then expose the container by including the following stanza within an NGINX config:

server {
    server_name bookshelf.jrpotter.com;

    listen 80;
    listen [::]:80;
    listen 443 ssl;
    listen [::]:443 ssl;

    ssl_certificate     /etc/letsencrypt/live/bookshelf.jrpotter.com/fullchain.pem;
    ssl_certificate_key /etc/letsencrypt/live/bookshelf.jrpotter.com/privkey.pem;

    location / {
        proxy_pass http://127.0.0.1:4001;
        proxy_set_header Connection $http_connection;
        proxy_set_header Upgrade $http_upgrade;
        proxy_set_header Host $host;
        proxy_set_header X-Real-IP $remote_addr;
        proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
        proxy_set_header X-Forwarded-Proto $scheme;
    }
}