diff --git a/flake.nix b/flake.nix index ff583bc..5bc52ef 100644 --- a/flake.nix +++ b/flake.nix @@ -26,7 +26,7 @@ let # Out zsh configuration directory. mkShell will pick up the .zshrc # from this directory. - zshDir = ./scripts/zsh; + zshDir = ./scripts; # Most of these overlays are do to bugs and problems # in upstream nixpkgs. But thanks to their design @@ -89,7 +89,7 @@ else []; }); - libbsd = prev.libbsd.overrideAttrs (old: { #old.NIX_LDFLAGS ++ + libbsd = prev.libbsd.overrideAttrs (old: { #old.NIX_LDFLAGS ++ NIX_LDFLAGS = if prev.stdenv.cc.isClang then [ "--undefined-version" ] else []; @@ -125,6 +125,8 @@ # Create a package set based on the build system pkgs = utils.get_pkgs system overlays; + nativePkgs = import nixpkgs { inherit system overlays; }; + # Create a stdenv based on LLVM 17 stdenv = pkgs.stdenvAdapters.overrideCC pkgs.stdenv pkgs.llvmPackages_17.clangUseLLVM; @@ -174,16 +176,19 @@ iwyu ]); - buildDevToolsDeps = (with pkgs; [ - ccache - git' - python3 + shellTools = (with pkgs; [ zsh zsh-autosuggestions zsh-autocomplete zsh-syntax-highlighting ]); + buildDevToolsDeps = (with pkgs; [ + ccache + git' + python3 + ]); + buildDeps = (with pkgs; [ gc zlib' @@ -195,16 +200,37 @@ testDeps = (with pkgs; [ gtest gmock + gbenchmark + ]); + + mathDeps = (with nativePkgs; [ + idris2 + agda + git + zsh + zsh-autosuggestions + zsh-autocomplete + zsh-syntax-highlighting ]); in { inherit pkgs; devShells.default = (pkgs.mkShell.override { stdenv = stdenv';}) { - nativeBuildInputs = buildDevToolsDeps ++ buildToolsDeps; + nativeBuildInputs = buildDevToolsDeps ++ buildToolsDeps ++ shellTools; buildInputs = buildDeps ++ testDeps; shellHook = '' - ZDOTDIR=${zshDir} zsh -d && exit + BUILDER= ZDOTDIR=${zshDir} zsh -d && exit + ''; + }; + + # This shell is gcc based and we use it only + # for the mathematics side of our design + devShells.math = nativePkgs.mkShell { + nativeBuildInputs = mathDeps; + shellHook = + '' + BUILDER=math ZDOTDIR=${zshDir} zsh -d -i && exit ''; }; diff --git a/scripts/.zshrc b/scripts/.zshrc new file mode 100644 index 0000000..0092162 --- /dev/null +++ b/scripts/.zshrc @@ -0,0 +1,92 @@ +#! /bin/zsh +# shellcheck disable=all +# Serene Programming Language +# +# Copyright (c) 2019-2024 Sameer Rahmani +# +# This program is free software; you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, version 2. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +mkdir -p "$HOME/.config/serene/" + +export HISTFILE="$HOME/.config/serene/.zsh_history" +export HISTFILESIZE=500 +export SAVEHIST=500 +export HISTSIZE=500 + +setopt HIST_IGNORE_DUPS +setopt NO_HIST_BEEP +setopt PROMPT_SUBST +setopt NO_BEEP +setopt AUTO_CD +setopt CORRECT +setopt SHARE_HISTORY +setopt HIST_IGNORE_ALL_DUPS +setopt NO_ERR_EXIT + +function user_prompt () { + if [ $UID != 0 ]; then + echo "%F{028}%F{002}> " + else + echo "%F{001}# " + fi +} + +autoload -U colors && colors +autoload -Uz compinit +compinit + +zstyle ':completion:*' auto-description 'specify: %d' +zstyle ':completion:*' completer _expand _complete _correct _approximate +zstyle ':completion:*' format 'Completing %d' +zstyle ':completion:*' group-name '' +if [ "$(uname 2> /dev/null)" = "Linux" ]; then + zstyle ':completion:*' menu select=2 eval "$(dircolors -b)" +fi +zstyle ':completion:*:default' list-colors ${(s.:.)LS_COLORS} +zstyle ':completion:*' list-colors '' +zstyle ':completion:*' list-prompt %SAt %p: Hit TAB for more, or the character to insert%s +zstyle ':completion:*' matcher-list '' 'm:{a-z}={A-Z}' 'm:{a-zA-Z}={A-Za-z}' 'r:|[._-]=* r:|=* l:|=*' +zstyle ':completion:*' menu select=long +zstyle ':completion:*' select-prompt %SScrolling active: current selection at %p%s +zstyle ':completion:*' use-compctl false +zstyle ':completion:*' verbose true + +zstyle ':completion:*:*:kill:*:processes' list-colors '=(#b) #([0-9]#)*=0=01;31' +zstyle ':completion:*:kill:*' command 'ps -u $USER -o pid,%cpu,tty,cputime,cmd' + +echo "Welcome to serene's development environment" + +PROMPT=' +%F{015}[%F{099}SERENE%F{015}][%F{198}$(git branch --show-current)%F{015}] +%F{005}%~%F{003} $(user_prompt)%f' + + +echo -e "\nSerene Development Shell $VERSION" +echo -e "\nCopyright (C) 2019-2024" +echo -e "Sameer Rahmani " +echo -e "Serene comes with ABSOLUTELY NO WARRANTY;" +echo -e "This is free software, and you are welcome" +echo -e "to redistribute it under certain conditions;" +echo -e "for details take a look at the LICENSE file.\n" +echo -e "\nUse the 'help' command to view a list of helpers.\n" + +ME=$(cd "$(dirname "$0")/." >/dev/null 2>&1 ; pwd -P) +export ME + +VERSION="0.9.0" + + +. "$ME/scripts/${BUILDER}functions.sh" + + +export PROMPT diff --git a/scripts/devfs_container_setup.sh b/scripts/devfs_container_setup.sh deleted file mode 100644 index e935b44..0000000 --- a/scripts/devfs_container_setup.sh +++ /dev/null @@ -1,142 +0,0 @@ -#! /bin/bash -# Serene Programming Language -# -# Copyright (c) 2019-2024 Sameer Rahmani -# -# This program is free software; you can redistribute it and/or modify -# it under the terms of the GNU General Public License as published by -# the Free Software Foundation, version 2. -# -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - -# ----------------------------------------------------------------------------- -# Commentary -# ----------------------------------------------------------------------------- -# This file installs all the dependencies on the guest container during the -# devfs initialization. - -set -e - -# shellcheck source=/dev/null -source /serene/scripts/utils.sh - - -function install_llvm() { - - wget https://apt.llvm.org/llvm.sh -O /root/llvm.sh - chmod +x llvm.sh - - /root/llvm.sh "${LLVM_VERSION}" all - - apt-get update --fix-missing - apt-get install -y --no-install-recommends \ - mlir-"${LLVM_VERSION}"-tools \ - libmlir-"${LLVM_VERSION}"-dev \ - libmlir-"${LLVM_VERSION}" \ - libmlir-"${LLVM_VERSION}"-dbgsym \ - liblld-"${LLVM_VERSION}" \ - liblld-"${LLVM_VERSION}"-dev \ - clang-format-"${LLVM_VERSION}" \ - clang-tidy-"${LLVM_VERSION}" - - ln -s "$(which lld-"${LLVM_VERSION}")" /usr/bin/lld - ln -s "$(which clang-"${LLVM_VERSION}")" /usr/bin/clang - ln -s "$(which clang++-"${LLVM_VERSION}")" /usr/bin/clang++ - ln -s "$(which clang-format-"${LLVM_VERSION}")" /usr/bin/clang-format - ln -s "$(which clang-tidy-"${LLVM_VERSION}")" /usr/bin/clang-tidy - ln -s "$(which mlir-tblgen-"${LLVM_VERSION}")" /usr/bin/mlir-tblgen - - MLIR_DIR="/usr/lib/llvm-${LLVM_VERSION}" - CMAKE_PREFIX_PATH="/usr/lib/llvm-${LLVM_VERSION}" - LD_LIBRARY_PATH="/usr/lib/llvm-${LLVM_VERSION}/lib/clang/${LLVM_VERSION}.0.0/lib/linux/" - CC=/usr/bin/clang - CXX=/usr/bin/clang++ -} - -function install_iwuy() { - mkdir -p /opt/iwuy - pushd /opt/iwuy - git clone https://github.com/include-what-you-use/include-what-you-use.git --depth 1 - mkdir build - pushd build - cmake -G Ninja -DCMAKE_PREFIX_PATH="/usr/lib/llvm-${LLVM_VERSION}" ../include-what-you-use - cmake --build . - cmake -P cmake_install.cmake - popd - popd - - rm -rf /opt/iwuy -} - -function install_boehm() { - mkdir -p /opt/boehm - pushd /opt/boehm - git clone https://github.com/ivmai/bdwgc.git --depth 1 --branch v8.2.0 - mkdir build - pushd build - cmake -G Ninja -DBUILD_SHARED_LIBS=OFF -Denable_cplusplus=ON -Denable_threads=ON \ - -Denable_gcj_support=OFF -Dinstall_headers=ON \ - -DCMAKE_POSITION_INDEPENDENT_CODE=ON ../bdwgc - cmake --build . --config Release - cmake -P cmake_install.cmake - popd - popd - - rm -rf /opt/boehm -} - -function main() { - pushd "/root" - - apt-get update - - apt-get install --no-install-recommends -y \ - gnupg \ - cmake \ - ccache \ - git \ - ninja-build \ - binutils \ - lsb-release \ - wget \ - software-properties-common \ - zlib1g \ - cppcheck \ - sudo \ - shellcheck \ - zlib1g-dev - - install_llvm - install_iwuy - install_boehm - popd - - info "Enabling passwordless sudo" - sed 's/%sudo.*/%sudo ALL=(ALL) NOPASSWD:ALL/' -i /etc/sudoers - - apt-get autoremove -y - apt-get clean -} - -if [ ! -f "/etc/llvm_version" ]; then - error "Can't find '/etc/llvm_version' on the container" - exit 1 -fi - -export LANG=C.UTF-8 -export LLVM_VERSION -export MLIR_DIR -export CMAKE_PREFIX_PATH -export LD_LIBRARY_PATH -export CC -export CXX - -LLVM_VERSION=$(cat /etc/llvm_version) - -main diff --git a/scripts/functions.sh b/scripts/functions.sh new file mode 100644 index 0000000..90532ef --- /dev/null +++ b/scripts/functions.sh @@ -0,0 +1,253 @@ +#! /bin/sh +# shellcheck disable=all +# Serene Programming Language +# +# Copyright (c) 2019-2024 Sameer Rahmani +# +# This program is free software; you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, version 2. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . +# +# ----------------------------------------------------------------------------- +# Commentary +# ----------------------------------------------------------------------------- +# This is the builder script for the Serene project. It makes it easier to +# interact with the CMake build scripts. +# +# In order to define a subcommand all you need to do is to define a function +# with the following syntax: +# +# function subcommand-name() { ## DESCRIPTION +# .. subcommand body .. +# } +# +# Make sure to provid one line of DESCRIPTION for the subcommand and use two "#" +# characters to start the description following by a space. Otherwise, your +# subcommand won't be registered +# + + +# shellcheck source=./utils.sh +source "$ME/scripts/utils.sh" + +# ----------------------------------------------------------------------------- +# CONFIG VARS +# ----------------------------------------------------------------------------- +# By default Clang is the compiler that we use and support. But you may use +# whatever you want. But just be aware of the fact that we might not be able +# to help you in case of any issue. +if [[ "$CC" = "" ]]; then + CC=$(which clang || echo "Clang_not_found") + export CC +fi +if [[ "$CXX" = "" ]]; then + CXX=$(which clang++ || echo "Clang++_not_found") + export CXX +fi + +BUILD_DIR_NAME="build" +export BUILD_DIR_NAME + +BUILD_DIR="$ME/$BUILD_DIR_NAME" +export BUILD_DIR + +SERENE_HOME_DIR="$HOME/.serene" +export SERENE_HOME_DIR + +# Serene subprojects. We use this array to run common tasks on all the projects +# like running the test cases +PROJECTS=(libserene serenec serene-repl serene-tblgen) + +# TODO: Add sloppiness to the cmake list file as well +CCACHE_SLOPPINESS="pch_defines,time_macros" +export CCACHE_SLOPPINESS + +ASAN_OPTIONS=check_initialization_order=1 +export ASAN_OPTIONS + +LSAN_OPTIONS=suppressions="$ME/.ignore_sanitize" +export LSAN_OPTIONS + +# ----------------------------------------------------------------------------- +# Helper functions +# ----------------------------------------------------------------------------- + +function gen_precompile_header_index() { + { + echo "// DO NOT EDIT THIS FILE: It is aute generated by './builder gen_precompile_index'" + echo "#ifndef SERENE_PRECOMPIL_H" + echo "#define SERENE_PRECOMPIL_H" + grep -oP "#include .llvm/.*" . -R|cut -d':' -f2|tail +2 + grep -oP "#include .mlir/.*" . -R|cut -d':' -f2|tail +2 + echo "#endif" + } > ./include/serene_precompiles.h +} + +function pushed_build() { + mkdir -p "$BUILD_DIR" + pushd "$BUILD_DIR" > /dev/null || return +} + + +function popd_build() { + popd > /dev/null || return +} + + +function build-gen() { + local args + + args=( + ) + + pushed_build + + info "Running: " + info "cmake -G Ninja" "${args[@]}" "$ME" "${@:2}" + cmake -G Ninja "${args[@]}" \ + "$ME" \ + "${@:2}" + popd_build +} + +# ----------------------------------------------------------------------------- +# Subcomaands +# ----------------------------------------------------------------------------- + +function compile() { ## Compiles the project using the generated build scripts + pushed_build + cmake --build . --parallel + popd_build +} + +function build() { ## Builds the project by regenerating the build scripts + local cpus + + rm -rf "$BUILD_DIR" + build-gen "debug" "$@" + pushed_build + + cpus=$(nproc) + cmake --build . -j "$cpus" + popd_build +} + +function build-20() { ## Builds the project using C++20 (will regenerate the build) + rm -rf "$BUILD_DIR" + pushed_build + build-gen "debug" -DCPP_20_SUPPORT=ON "$@" + cmake --build . + popd_build +} + +function build-tidy() { ## Builds the project using clang-tidy (It takes longer than usual) + build "-DSERENE_ENABLE_TIDY=ON" "${@:2}" +} + +function build-release() { ## Builds the project in "Release" mode + rm -rf "$BUILD_DIR" + pushed_build + build-gen "release" "$@" + cmake --build . --config Release + popd_build +} + +function build-docs() { ## Builds the documentation of Serene + rm -rf "$BUILD_DIR" + pip install -r "$ME/docs/requirements.txt" + pushed_build + build-gen "debug" -DSERENE_ENABLE_DOCS=ON "$@" + cmake --build . --parallel + popd_build +} + +function serve-docs() { ## Serve the docs directory from build dir + python -m http.server --directory "$BUILD_DIR/docs/sphinx/" +} + +function clean() { ## Cleans up the source dir and removes the build + git clean -dxf +} + +function run() { ## Runs `serene` and passes all the given aruguments to it + "$BUILD_DIR"/serene/serene "$@" +} + +function lldb-run() { ## Runs `serenec` under lldb + lldb -- "$BUILD_DIR"/serenec/serenec "$@" +} + +function repl() { ## Runs `serene-repl` and passes all the given aruguments to it + "$BUILD_DIR"/serene-repl/serene-repl "$@" +} + +function memcheck-serene() { ## Runs `valgrind` to check `serenec` birany + export ASAN_FLAG="" + build + pushed_build + valgrind --tool=memcheck --leak-check=yes --trace-children=yes "$BUILD_DIR"/bin/serenec "$@" + popd_build +} + +function tests() { ## Runs all the test cases + if [[ "$1" == "all" || "$1" == "" ]]; then + info "Run the entire test suit" + for proj in "${PROJECTS[@]}"; do + local test_file="$BUILD_DIR/$proj/tests/${proj}Tests" + + if [[ -f "$test_file" ]]; then + eval "$test_file ${*:2}" + fi + done + else + eval "$BUILD_DIR/$1/tests/$1Tests ${*:2}" + fi +} + +function build-tests() { ## Generates and build the project including the test cases + rm -rf "$BUILD_DIR" + pushed_build + build-gen "debug" -DSERENE_BUILD_TESTING=ON "$@" + cmake --build . --parallel + popd_build +} + + +function setup() { ## Setup the working directory and make it ready for development + local args + if [[ "$SERENE_CI" == "true" ]]; then + args=--break-system-packages + fi + if command -v python3 >/dev/null 2>&1; then + pip install "$args" pre-commit + pre-commit install + else + error "Python is required to setup pre-commit" + fi +} + +function scan-build() { ## Runs the `scan-build` utility to analyze the build process + rm -rf "$BUILD_DIR" + build-gen + pushed_build + # The scan-build utility scans the build for bugs checkout the man page + scan-build --force-analyze-debug-code --use-analyzer="$CC" cmake --build . + popd_build +} + + +function help() { ## Print out this help message + echo "Commands:" + grep -E '^function [a-zA-Z0-9_-]+\(\) \{ ## .*$$' "$ME/scripts/functions.sh" | \ + sort | \ + sed 's/^function \([a-zA-Z0-9_-]*\)() { ## \(.*\)/\1:\2/' | \ + awk 'BEGIN {FS=":"}; {printf "\033[36m%-30s\033[0m %s\n", $1, $2}' +} diff --git a/scripts/mathfunctions.sh b/scripts/mathfunctions.sh new file mode 100644 index 0000000..5c951a0 --- /dev/null +++ b/scripts/mathfunctions.sh @@ -0,0 +1,49 @@ +#! /bin/sh +# shellcheck disable=all +# Serene Programming Language +# +# Copyright (c) 2019-2024 Sameer Rahmani +# +# This program is free software; you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, version 2. +# +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +# GNU General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . +# +# ----------------------------------------------------------------------------- +# Commentary +# ----------------------------------------------------------------------------- +# This is the builder script for the Serene project. It makes it easier to +# interact with the CMake build scripts. +# +# In order to define a subcommand all you need to do is to define a function +# with the following syntax: +# +# function subcommand-name() { ## DESCRIPTION +# .. subcommand body .. +# } +# +# Make sure to provid one line of DESCRIPTION for the subcommand and use two "#" +# characters to start the description following by a space. Otherwise, your +# subcommand won't be registered +# + + +# shellcheck source=./utils.sh +source "$ME/scripts/utils.sh" + + + +function help() { ## Print out this help message + echo "Commands:" + grep -E '^function [a-zA-Z0-9_-]+\(\) \{ ## .*$$' "$ME/scripts/mathfunctions.sh" | \ + sort | \ + sed 's/^function \([a-zA-Z0-9_-]*\)() { ## \(.*\)/\1:\2/' | \ + awk 'BEGIN {FS=":"}; {printf "\033[36m%-30s\033[0m %s\n", $1, $2}' +} diff --git a/scripts/utils.sh b/scripts/utils.sh index b917f96..bf8d29d 100644 --- a/scripts/utils.sh +++ b/scripts/utils.sh @@ -15,7 +15,6 @@ # You should have received a copy of the GNU General Public License # along with this program. If not, see . -set -e # ----------------------------------------------------------------------------- # Helper functions @@ -71,66 +70,3 @@ function get_version() { git ls-tree HEAD "$1" | awk '{ print $3 }' } - -function http_push() { - if [[ -z "$DEV_HEROES_TOKEN" ]]; then - error "\$DEV_HEROES_TOKEN is not set." - exit 1 - fi - - local pkg_name - local version - - pkg_name="$1" - version="$2" - - curl "$DEV_HEROES/api/packages/serene/generic/$pkg_name/$version/$pkg_name.$version.zstd" \ - --upload-file "$pkg_name.$version.zstd" \ - --progress-bar \ - -H "accept: application/json" \ - -H "Authorization: token $DEV_HEROES_TOKEN" \ - -H "Content-Type: application/json" -} - -function http_pull() { - local pkg_name - local version - local output - local url - - pkg_name="$1" - version="$2" - output="$3" - url="$DEV_HEROES/api/packages/serene/generic/$pkg_name/$version/$pkg_name.$version.tar.zstd" - - info "Fetching '$url'..." - - if curl "$url" --fail --progress-bar -o "$output"; then - return 0 - else - return 4 - fi -} - -function clone_dep() { - local dest - local repo - local version - repo="$1" - version="$2" - dest="$3" - - if [[ -d "$dest" ]]; then - return - fi - - #mkdir -p "$dest" - - #git init -b master - git clone --depth=1 "$repo" "$dest" - _push "$dest" - #git remote add origin "$repo" - git fetch --depth=1 --filter=tree:0 origin "$version" - git reset --hard FETCH_HEAD - _pop -} diff --git a/scripts/zsh/.zshrc b/scripts/zsh/.zshrc deleted file mode 100644 index c69a18b..0000000 --- a/scripts/zsh/.zshrc +++ /dev/null @@ -1,72 +0,0 @@ -#! /bin/zsh -# shellcheck disable=all -# Serene Programming Language -# -# Copyright (c) 2019-2024 Sameer Rahmani -# -# This program is free software; you can redistribute it and/or modify -# it under the terms of the GNU General Public License as published by -# the Free Software Foundation, version 2. -# -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - -mkdir -p "$HOME/.config/serene/" - -export HISTFILE="$HOME/.config/serene/.zsh_history" -export HISTFILESIZE=500 -export SAVEHIST=500 -export HISTSIZE=500 - -setopt HIST_IGNORE_DUPS -setopt NO_HIST_BEEP -setopt PROMPT_SUBST -setopt NO_BEEP -setopt AUTO_CD -setopt CORRECT -setopt SHARE_HISTORY -setopt HIST_IGNORE_ALL_DUPS - -function user_prompt () { - if [ $UID != 0 ]; then - echo "%F{028}%F{002}> " - else - echo "%F{001}# " - fi -} - -autoload -U colors && colors -autoload -Uz compinit -compinit - -# zstyle ':completion:*' auto-description 'specify: %d' -# zstyle ':completion:*' completer _expand _complete _correct _approximate -# zstyle ':completion:*' format 'Completing %d' -# zstyle ':completion:*' group-name '' -# if [ "$(uname 2> /dev/null)" = "Linux" ]; then -# zstyle ':completion:*' menu select=2 eval "$(dircolors -b)" -# fi -# zstyle ':completion:*:default' list-colors ${(s.:.)LS_COLORS} -# zstyle ':completion:*' list-colors '' -# zstyle ':completion:*' list-prompt %SAt %p: Hit TAB for more, or the character to insert%s -# zstyle ':completion:*' matcher-list '' 'm:{a-z}={A-Z}' 'm:{a-zA-Z}={A-Za-z}' 'r:|[._-]=* r:|=* l:|=*' -# zstyle ':completion:*' menu select=long -# zstyle ':completion:*' select-prompt %SScrolling active: current selection at %p%s -# zstyle ':completion:*' use-compctl false -# zstyle ':completion:*' verbose true - -# zstyle ':completion:*:*:kill:*:processes' list-colors '=(#b) #([0-9]#)*=0=01;31' -# zstyle ':completion:*:kill:*' command 'ps -u $USER -o pid,%cpu,tty,cputime,cmd' - -echo "Welcome to serene's development environment" - -PROMPT=' -%F{015}[%F{099}SERENE%F{015}][%F{198}$(git branch --show-current)%F{015}] -%F{005}%~%F{003} $(user_prompt)%f' - -export PROMPT diff --git a/serene/src/types.h b/serene/src/types.h index 7bf4a4e..082f686 100644 --- a/serene/src/types.h +++ b/serene/src/types.h @@ -23,6 +23,19 @@ #include +// Steps for defining a new type: +// 1. Define the type former +// 2. Type constructors +// 3. Type eliminators +// 4. Computation rule (eval rules) +// 5. (optional) A uniqueness principle + +// Types to create: +// Universe +// Unit Type +// Dependent Function Type +// Pair (or even better, records) + typedef struct { const TypeID id; const char *name;