commit bbf21e920156039b3a36e6687397bf25f51e8a16 Author: engboris Date: Thu Jun 6 00:37:36 2024 +0200 Initial guide diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..73ab876 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +public/ +resources/ diff --git a/.hugo_build.lock b/.hugo_build.lock new file mode 100644 index 0000000..e69de29 diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..6b4181e --- /dev/null +++ b/Makefile @@ -0,0 +1,6 @@ +build: + hugo --minify --theme hugo-book + +watch: + hugo server --minify --theme hugo-book + diff --git a/archetypes/default.md b/archetypes/default.md new file mode 100644 index 0000000..c6f3fce --- /dev/null +++ b/archetypes/default.md @@ -0,0 +1,5 @@ ++++ +title = '{{ replace .File.ContentBaseName "-" " " | title }}' +date = {{ .Date }} +draft = true ++++ diff --git a/content/_index.md b/content/_index.md new file mode 100644 index 0000000..bf57927 --- /dev/null +++ b/content/_index.md @@ -0,0 +1,23 @@ +--- +title: TS Guide +type: docs +--- + +# Welcome to TS Guide + +The purpose of this guide is to make you familiar with Girard's recent works +through programming and exercises. + +Note that everything in this guide is my own interpretation and is not +necessarily perfect faithful to Girard's point of view. + +Also keep in mind that the development of transcendental syntax is currently +very unstable. For that reason, this guide is subject to constant changes. +I created this guide because I wanted other people to be part of the process of +understanding Girard's transcendental syntax by playing with it and developing +new ideas. + +Enjoy! + + +Boris Eng. \ No newline at end of file diff --git a/content/docs/introduction/_index.md b/content/docs/introduction/_index.md new file mode 100644 index 0000000..7864f76 --- /dev/null +++ b/content/docs/introduction/_index.md @@ -0,0 +1,5 @@ +--- +title: "Introduction" +bookFlatSection: true +weight: 1 +--- diff --git a/content/docs/introduction/install.md b/content/docs/introduction/install.md new file mode 100644 index 0000000..17f9b4b --- /dev/null +++ b/content/docs/introduction/install.md @@ -0,0 +1,16 @@ +--- +title: Install LSC +weight: 2 +--- + +# Install LSC + +To install the Large Star Collider (LSC), go to this git repository: + +https://github.com/engboris/large-star-collider + +You can either compile the LSC from sources or download a released binary. +- For Linux x86-x64: https://github.com/engboris/large-star-collider/tags + +You can then write your programs on any text file and follow the instructions +in the `README.md` file of the Github repository to execute them! diff --git a/content/docs/introduction/what.md b/content/docs/introduction/what.md new file mode 100644 index 0000000..b0af777 --- /dev/null +++ b/content/docs/introduction/what.md @@ -0,0 +1,18 @@ +--- +title: "What it is about" +weight: 1 +--- + +# What it is about + +## Transcendental syntax + +(soon) + +## Stellar resolution + +(soon) + +## Large star collider + +(soon) \ No newline at end of file diff --git a/content/docs/playing/_index.md b/content/docs/playing/_index.md new file mode 100644 index 0000000..38bfe7f --- /dev/null +++ b/content/docs/playing/_index.md @@ -0,0 +1,5 @@ +--- +title: "Playing with stars" +bookFlatSection: true +weight: 1 +--- diff --git a/content/docs/playing/interaction.md b/content/docs/playing/interaction.md new file mode 100644 index 0000000..f489f1a --- /dev/null +++ b/content/docs/playing/interaction.md @@ -0,0 +1,127 @@ +--- +title: "Interaction" +weight: 2 +--- + +# Matchable rays + +Usually, in the theory of term unification, we say that two terms (which are +basically rays without polarities) are *unifiable* where there a substitution +of variables making them equal. For instance `f(X)` and `f(h(Y))` are unifiable +with the substitution `{X:=h(Y)}` replacing `X` by `h(Y)`. + +We are usually interested in the most general substitution. We could have +`{X:=h(c(a)); Y:={c(a)}` but it would be less general. + +In the same fashion, we say that two rays are *matchable* when their underlying +terms (obtained by dropping polarities) are unifiable but we also want opposite +polarities to face each other instead of looking for equal symbols: we want +symbols prefixed with `+` to match same symbols but prefixed with `-`: + +- `+f(X)` and `-f(h(a))` are matchable with `{X:=h(a)}`; +- `f(X)` and `f(h(a))` are not matchable; +- `+f(X)` and `+f(h(a))` are not matchable; +- `+f(+h(X))` and `-f(-h(a))` are matchable with `{X:=a}`; +- `+f(+h(X))` and `-f(-h(+a))` are matchable with `{X:=+a}`; + +# Fusion + +Stars are able to interact, through an operation called *fusion*, by using the +principle of Robinson's resolution rule. We define an operator `` with +connects the `i`th ray of a star to the `j`th ray of another star. + +Fusion is defined as follows for matchable rays `r` and `r'`: +``` +r r1 ... rk <0,0> r' r1' ... rk' == theta(r1) ... theta(rk) theta(r1') ... theta(rk') +``` + +where `theta` is the most general substitution induced by `r` and `r'`. + +Notice that: +- `r` and `r'` interact and are annihilated; +- the two stars are merged; +- the substitution resolving the conflict between `r` and `r'` is propagated to +adjacent rays. + +For example: +``` +X +f(X) <1,0> -f(a) == a +``` + +{{< hint info >}} +This corresponds to the cut rule for first-order logic except that we are +in a logic-agnostic setting (our symbols do not hold any meaning). +{{< /hint >}} + +# Execution + +You have to put a focus on some stars to start a computation as in: +``` +X1, f(X1); ++a(X2 Y2); +@-h(f(X3 Y3)) +a(+f(X4) h(-f(X4))); +``` + +An *interaction configuration* is an expression `R |- I'` where: +- `R` is a static constellation called *reference constellation*. It corresponds +to unmarked stars; +- `I` is a dynamic constellation called *interaction space*. It corresponds to +all stars marked by a focus symbol `@`. It can be seen as a "working space". + +The LSC execute constellations by looking for copies of partners in `R` for +each rays of `I`, as follows: +1. select a ray `ri` in a star `s` of `I`; +2. look for possible connections with rays `rj` belonging to stars in `R`; +3. duplicate `s` so that there is exactly one copy of `s` in `I` for every `rj`; +4. replace every copy by its fusion `s s'`, where `s'` is the star to + which `rj` belongs; +5. repeat until there is no possible interaction in `I`. + +The result of execution consists of all *neutral* stars that remain in `I`, i.e. +those without any polarized rays. Indeed, polarized stars are ignored/removed +because they correspond to *unfinished* (or stuck) computations. + +# Example + +We want to execute the following constellation: +``` ++7(l:X) +7(r:X); 3(X) +8(l:X); @+8(r:X) 6(X); +-7(X) -8(X); +``` + +We distinguish an interaction space on which we focus interaction and a +reference constellation where we copy possible partners. We prefix `>>` for +selected rays. We have: +``` ++7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) >>-8(X) |- >>+8(r:X) 6(X); +``` + +``` ++7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- -7(r:X) 6(X); +``` + +``` ++7(l:X) >>+7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- >>-7(r:X) 6(X); +``` + +``` ++7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- +7(l:X) 6(X); +``` + +``` ++7(l:X) +7(r:X); 3(X) +8(l:X); >>-7(X) -8(X) |- >>+7(l:X) 6(X); +``` + +``` ++7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- -8(l:X) 6(X); +``` + +``` ++7(l:X) +7(r:X); 3(X) >>+8(l:X); -7(X) -8(X) |- >>-8(l:X) 6(X); +``` + +``` ++7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- 3(X) 6(X); +``` + +The result of the computation is `3(X) 6(X);`. \ No newline at end of file diff --git a/content/docs/playing/syntax.md b/content/docs/playing/syntax.md new file mode 100644 index 0000000..07610e4 --- /dev/null +++ b/content/docs/playing/syntax.md @@ -0,0 +1,67 @@ +--- +title: "Syntax" +weight: 1 +--- + +# Rays + +Either a variable (uppercase, possibly followed by digits) or a polarised (+/-) +or unpolarised (lowercase, possibly containing `_` and digits) +function symbol applied to other rays (or nothing in case of constants): + +`X`, `a`, `f(X)`, `+f(X)`, `-f(-h(a, Y1), X2)`, `+add_dec(0, 2, 2)`. + +Commas can be omitted: + +`-f(-h(a Y1) X2)`, `+add_dec(0 2 2)`, `string(hello i am X)`. + +# Cons + +There is a special binary infix function symbol `:` which can be used to +concatenate rays: + +`a:X`, `a:b:b:X`, `f(a:X):+f(0:1:X):-f(Y)`. + +# Stars + +An unordered sequence of rays ending with a semicolon `;`: + +``` +X a +f(X); +``` + +# Constellations + +An unordered sequence of stars: + +``` +X a +f(X); -f(-h(a Y1) X2); ++add_dec(0 2 2); +``` + +All variables are local to their stars, hence the occurrences of `X` in the +first line are distinct from the one in the second line. + +# Focus + +You can prefix stars with a `@` symbol to put a *focus* over them. This will +affect the behaviour of computation: + +``` +@X a +f(X); +@-f(-h(a Y1) X2); ++add_dec(0 2 2); +``` + +# Comments + +``` +'this is a comment on a single line +'this is another comment + +''' +this is a +comment on +several lines +''' +``` \ No newline at end of file diff --git a/hugo.toml b/hugo.toml new file mode 100644 index 0000000..f01db71 --- /dev/null +++ b/hugo.toml @@ -0,0 +1,3 @@ +baseURL = 'https://tsguide.refl.fr/' +languageCode = 'fr-FR' +title = 'TS Guide' diff --git a/themes/hugo-book/.github/workflows/main.yml b/themes/hugo-book/.github/workflows/main.yml new file mode 100644 index 0000000..86ffb38 --- /dev/null +++ b/themes/hugo-book/.github/workflows/main.yml @@ -0,0 +1,34 @@ +name: Build with Hugo + +on: [push, pull_request] + +jobs: + build: + runs-on: ubuntu-latest + strategy: + matrix: + hugo-version: + - 'latest' + - '0.79.0' + steps: + - uses: actions/checkout@v4 + with: + submodules: true # Fetch Hugo themes (true OR recursive) + fetch-depth: 0 # Fetch all history for .GitInfo and .Lastmod + + - name: Setup Hugo + uses: peaceiris/actions-hugo@v2 + with: + hugo-version: ${{ matrix.hugo-version }} + extended: true + + - name: Run Hugo + working-directory: exampleSite + run: hugo --themesDir ../.. + + # - name: Deploy + # uses: peaceiris/actions-gh-pages@v3 + # with: + # github_token: ${{ secrets.GITHUB_TOKEN }} + # publish_dir: ./public + diff --git a/themes/hugo-book/.gitignore b/themes/hugo-book/.gitignore new file mode 100644 index 0000000..5944200 --- /dev/null +++ b/themes/hugo-book/.gitignore @@ -0,0 +1,4 @@ +public/ +exampleSite/public/ +.DS_Store +.hugo_build.lock diff --git a/themes/hugo-book/LICENSE b/themes/hugo-book/LICENSE new file mode 100644 index 0000000..e7a669a --- /dev/null +++ b/themes/hugo-book/LICENSE @@ -0,0 +1,20 @@ +The MIT License (MIT) + +Copyright (c) 2018 Alex Shpak + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +the Software, and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/themes/hugo-book/README.md b/themes/hugo-book/README.md new file mode 100644 index 0000000..7e159a4 --- /dev/null +++ b/themes/hugo-book/README.md @@ -0,0 +1,358 @@ +# Hugo Book Theme + +[![Hugo](https://img.shields.io/badge/hugo-0.79-blue.svg)](https://gohugo.io) +[![License: MIT](https://img.shields.io/badge/License-MIT-blue.svg)](LICENSE) +![Build with Hugo](https://github.com/alex-shpak/hugo-book/workflows/Build%20with%20Hugo/badge.svg) + +### [Hugo](https://gohugo.io) documentation theme as simple as plain book + +![Screenshot](https://github.com/alex-shpak/hugo-book/blob/master/images/screenshot.png) + +- [Features](#features) +- [Requirements](#requirements) +- [Installation](#installation) +- [Menu](#menu) +- [Blog](#blog) +- [Configuration](#configuration) +- [Shortcodes](#shortcodes) +- [Versioning](#versioning) +- [Contributing](#contributing) + +## Features + +- Clean simple design +- Light and Mobile-Friendly +- Multi-language support +- Customisable +- Zero initial configuration +- Handy shortcodes +- Comments support +- Simple blog and taxonomy +- Primary features work without JavaScript +- Dark Mode + +## Requirements + +- Hugo 0.79 or higher +- Hugo extended version, read more [here](https://gohugo.io/news/0.48-relnotes/) + +## Installation + +### Install as git submodule +Navigate to your hugo project root and run: + +``` +git submodule add https://github.com/alex-shpak/hugo-book themes/hugo-book +``` + +Then run hugo (or set `theme = "hugo-book"`/`theme: hugo-book` in configuration file) + +``` +hugo server --minify --theme hugo-book +``` + +### Install as hugo module + +You can also add this theme as a Hugo module instead of a git submodule. + +Start with initializing hugo modules, if not done yet: +``` +hugo mod init github.com/repo/path +``` + +Navigate to your hugo project root and add [module] section to your `config.toml`: + +```toml +[module] +[[module.imports]] +path = 'github.com/alex-shpak/hugo-book' +``` + +Then, to load/update the theme module and run hugo: + +```sh +hugo mod get -u +hugo server --minify +``` + +### Creating site from scratch + +Below is an example on how to create a new site from scratch: + +```sh +hugo new site mydocs; cd mydocs +git init +git submodule add https://github.com/alex-shpak/hugo-book themes/hugo-book +cp -R themes/hugo-book/exampleSite/content.en/* ./content +``` + +```sh +hugo server --minify --theme hugo-book +``` + +## Menu + +### File tree menu (default) + +By default, the theme will render pages from the `content/docs` section as a menu in a tree structure. +You can set `title` and `weight` in the front matter of pages to adjust the order and titles in the menu. + +### Leaf bundle menu (Deprecated, to be removed in June 2022) + +You can also use leaf bundle and the content of its `index.md` file as menu. +Given you have the following file structure: + +``` +├── content +│ ├── docs +│ │ ├── page-one.md +│ │ └── page-two.md +│ └── posts +│ ├── post-one.md +│ └── post-two.md +``` + +Create a file `content/menu/index.md` with the content: + +```md ++++ +headless = true ++++ + +- [Book Example]({{< relref "/docs/" >}}) + - [Page One]({{< relref "/docs/page-one" >}}) + - [Page Two]({{< relref "/docs/page-two" >}}) +- [Blog]({{< relref "/posts" >}}) +``` + +And Enable it by setting `BookMenuBundle: /menu` in Site configuration. + +- [Example menu](https://github.com/alex-shpak/hugo-book/blob/master/exampleSite/content.en/menu/index.md) +- [Example config file](https://github.com/alex-shpak/hugo-book/blob/master/exampleSite/config.yaml) +- [Leaf bundles](https://gohugo.io/content-management/page-bundles/) + +## Blog + +A simple blog is supported in the section `posts`. +A blog is not the primary usecase of this theme, so it has only minimal features. + +## Configuration + +### Site Configuration + +There are a few configuration options that you can add to your `config.toml` file. +You can also see the `yaml` example [here](https://github.com/alex-shpak/hugo-book/blob/master/exampleSite/config.yaml). + +```toml +# (Optional) Set Google Analytics if you use it to track your website. +# Always put it on the top of the configuration file, otherwise it won't work +googleAnalytics = "UA-XXXXXXXXX-X" + +# (Optional) If you provide a Disqus shortname, comments will be enabled on +# all pages. +disqusShortname = "my-site" + +# (Optional) Set this to true if you use capital letters in file names +disablePathToLower = true + +# (Optional) Set this to true to enable 'Last Modified by' date and git author +# information on 'doc' type pages. +enableGitInfo = true + +# (Optional) Theme is intended for documentation use, therefore it doesn't render taxonomy. +# You can remove related files with config below +disableKinds = ['taxonomy', 'taxonomyTerm'] + +[params] + # (Optional, default light) Sets color theme: light, dark or auto. + # Theme 'auto' switches between dark and light modes based on browser/os preferences + BookTheme = 'light' + + # (Optional, default true) Controls table of contents visibility on right side of pages. + # Start and end levels can be controlled with markup.tableOfContents setting. + # You can also specify this parameter per page in front matter. + BookToC = true + + # (Optional, default none) Set the path to a logo for the book. If the logo is + # /static/logo.png then the path would be 'logo.png' + BookLogo = 'logo.png' + + # (Optional, default none) Set leaf bundle to render as side menu + # When not specified file structure and weights will be used + # Deprecated, to be removed in June 2022 + BookMenuBundle = '/menu' + + # (Optional, default docs) Specify section of content to render as menu + # You can also set value to "*" to render all sections to menu + BookSection = 'docs' + + # Set source repository location. + # Used for 'Last Modified' and 'Edit this page' links. + BookRepo = 'https://github.com/alex-shpak/hugo-book' + + # Specifies commit portion of the link to the page's last modified commit hash for 'doc' page + # type. + # Required if 'BookRepo' param is set. + # Value used to construct a URL consisting of BookRepo/BookCommitPath/ + # Github uses 'commit', Bitbucket uses 'commits' + BookCommitPath = 'commit' + + # Enable 'Edit this page' links for 'doc' page type. + # Disabled by default. Uncomment to enable. Requires 'BookRepo' param. + # Path must point to the site directory. + BookEditPath = 'edit/master/exampleSite' + + # (Optional, default January 2, 2006) Configure the date format used on the pages + # - In git information + # - In blog posts + BookDateFormat = 'Jan 2, 2006' + + # (Optional, default true) Enables search function with flexsearch, + # Index is built on fly, therefore it might slowdown your website. + # Configuration for indexing can be adjusted in i18n folder per language. + BookSearch = true + + # (Optional, default true) Enables comments template on pages + # By default partials/docs/comments.html includes Disqus template + # See https://gohugo.io/content-management/comments/#configure-disqus + # Can be overwritten by same param in page frontmatter + BookComments = true + + # /!\ This is an experimental feature, might be removed or changed at any time + # (Optional, experimental, default false) Enables portable links and link checks in markdown pages. + # Portable links meant to work with text editors and let you write markdown without {{< relref >}} shortcode + # Theme will print warning if page referenced in markdown does not exists. + BookPortableLinks = true + + # /!\ This is an experimental feature, might be removed or changed at any time + # (Optional, experimental, default false) Enables service worker that caches visited pages and resources for offline use. + BookServiceWorker = true +``` + +### Multi-Language Support + +Theme supports Hugo's [multilingual mode](https://gohugo.io/content-management/multilingual/), just follow configuration guide there. You can also tweak search indexing configuration per language in `i18n` folder. + +### Page Configuration + +You can specify additional params in the front matter of individual pages: + +```toml +# Set type to 'docs' if you want to render page outside of configured section or if you render section other than 'docs' +type = 'docs' + +# Set page weight to re-arrange items in file-tree menu (if BookMenuBundle not set) +weight = 10 + +# (Optional) Set to 'true' to mark page as flat section in file-tree menu (if BookMenuBundle not set) +bookFlatSection = false + +# (Optional) Set to hide nested sections or pages at that level. Works only with file-tree menu mode +bookCollapseSection = true + +# (Optional) Set true to hide page or section from side menu (if BookMenuBundle not set) +bookHidden = false + +# (Optional) Set 'false' to hide ToC from page +bookToC = true + +# (Optional) If you have enabled BookComments for the site, you can disable it for specific pages. +bookComments = true + +# (Optional) Set to 'false' to exclude page from search index. +bookSearchExclude = true + +# (Optional) Set explicit href attribute for this page in a menu (if BookMenuBundle not set) +bookHref = '' +``` + +### Partials + +There are layout partials available for you to easily override components of the theme in `layouts/partials/`. + +In addition to this, there are several empty partials you can override to easily add/inject code. + +| Empty Partial | Placement | +| -------------------------------------------------- | ------------------------------------------- | +| `layouts/partials/docs/inject/head.html` | Before closing `` tag | +| `layouts/partials/docs/inject/body.html` | Before closing `` tag | +| `layouts/partials/docs/inject/footer.html` | After page footer content | +| `layouts/partials/docs/inject/menu-before.html` | At the beginning of `