Merge pull request #266 from Beluga-lang/feature/merge-from-main

Feature/merge from main

.github/workflows/ci_build.yaml

@@ -30,7 +30,7 @@ jobs:
       contents: write
     env:
       REGISTRY: "ghcr.io"
-      IMAGE_TAG: "beluga-lang/mcltt:main"
+      IMAGE_TAG: "beluga-lang/mctt:main"
       # Only deploy if the build follows from pushing to one of main branches
       DOC_DEPLOY: ${{ (github.ref_name == 'main' || startsWith(github.ref_name, 'ext/')) && 'true' || 'false' }}
       DOC_DEPLOY_DEST: ${{ startsWith(github.ref_name, 'ext/') && github.ref_name || '' }}
@@ -73,8 +73,8 @@ jobs:
                 mv theories/dep.html html/dep.html
                 cp assets/styling.css html/styling.css
                 cp -r assets/images html/images
-                sed -i 's!\[Coqdoc\](https://beluga-lang\.github\.io/McLTT/dep\.html)![Coqdoc](dep.html)!' README.md
-                pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McLTT: A Bottom-up Approach to Implementing A Proof Assistant' -t html --css styling.css -o html/index.html
+                sed -i 's!\[Coqdoc\](https://beluga-lang\.github\.io/McTT/dep\.html)![Coqdoc](dep.html)!' README.md
+                pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McTT: Building A Correct-By-Construction Proof Checkers For Type Theories' -t html --css styling.css -o html/index.html
               fi
             endGroup
             startGroup "Run inline tests"

README.md

@@ -1,23 +1,23 @@
-# McLTT: A Bottom-up Approach to Implementing A Proof Assistant
+# McTT: Building A Correct-By-Construction Proof Checkers For Type Theories
 
-McLTT is a verified, runnable typechecker for Martin-Löf type theory. This project provides an executable, to which we can feed
+McTT is a verified, runnable typechecker for Martin-Löf type theory. This project provides an executable, to which we can feed
 a program in Martin-Löf type theory to check whether this
-program has the specified type. McLTT is novel in that it is implemented and verified in
+program has the specified type. McTT is novel in that it is implemented and verified in
 Coq. More specifically, we proved that the typechecking algorithm extracted from Coq is
 sound and complete: a program passes typechecker if and only if it is a well-typed
 program in MLTT. This is the first verified proof assistant (despite being
 elementary) and serves as a basis for future extensions. 
 
 ## Online Documentation
 
-We have generated a [Coqdoc](https://beluga-lang.github.io/McLTT/dep.html) for browsing our Coq proof.
+We have generated a [Coqdoc](https://beluga-lang.github.io/McTT/dep.html) for browsing our Coq proof.
 
 ## Architecture
 
-McLTT has the following architecture:
+McTT has the following architecture:
 
 ```
-    | source code of McLTT
+    | source code of McTT
     v
 +-------+
 | lexer |          OCaml code generated by ocamllex
@@ -58,6 +58,7 @@ implementation.
 We recommend to install dependencies in the following way:
 
 ```bash
+opam update
 opam switch create coq-8.20.0 4.14.2
 opam pin add coq 8.20.0
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -75,11 +76,11 @@ possible.
 
 Once `make` finishes, you can run the binary:
 ```
-dune exec mcltt examples/nary.mcl # or your own example
+dune exec mctt examples/nary.mctt # or your own example
 ```
 or more directly
 ```
-_build/default/driver/mcltt.exe examples/nary.mcl # or your own example
+_build/default/driver/mctt.exe examples/nary.mctt # or your own example
 ```
 
 To build Coq proof only, you can go into and only build the `theories` directory:

assets/include.html

@@ -16,7 +16,7 @@
      var header = $(`<div id="header_wrap" class="outer">
         <header class="inner">
           
-            <a id="forkme_banner" href="https://github.com/Beluga-lang/McLTT">Fork on GitHub</a>
+            <a id="forkme_banner" href="https://github.com/Beluga-lang/McTT">Fork on GitHub</a>
           ${h1elem.outerHTML}
         </header>
     </div>`);

driver/Lexer.mli

@@ -1,7 +1,7 @@
 val format_position : Format.formatter -> Lexing.position -> unit
 val format_range : Format.formatter -> Lexing.position * Lexing.position -> unit
-val format_token : Format.formatter -> MclttExtracted.Parser.token -> unit
-val read : Lexing.lexbuf -> MclttExtracted.Parser.token
+val format_token : Format.formatter -> McttExtracted.Parser.token -> unit
+val read : Lexing.lexbuf -> McttExtracted.Parser.token
 
 val lexbuf_to_token_buffer :
-  Lexing.lexbuf -> MclttExtracted.Parser.MenhirLibParser.Inter.buffer
+  Lexing.lexbuf -> McttExtracted.Parser.MenhirLibParser.Inter.buffer

driver/Lexer.mll

@@ -1,6 +1,6 @@
 {
   open Lexing
-  open MclttExtracted.Parser
+  open McttExtracted.Parser
 
   let get_range lexbuf = (lexbuf.lex_start_p, lexbuf.lex_curr_p)
 

driver/Main.ml

@@ -1,5 +1,5 @@
-module Parser = MclttExtracted.Parser
-module Entrypoint = MclttExtracted.Entrypoint
+module Parser = McttExtracted.Parser
+module Entrypoint = McttExtracted.Entrypoint
 open Parser
 open MenhirLibParser.Inter
 open Entrypoint

driver/Mcltt.ml → driver/Mctt.ml

@@ -1,4 +1,4 @@
-open Mcltt.Main
+open Mctt.Main
 
 let () =
   if Array.length Sys.argv <> 2

driver/PrettyPrinter.ml

@@ -1,7 +1,7 @@
-open MclttExtracted.Entrypoint
-open MclttExtracted.Syntax
-module Parser = MclttExtracted.Parser
-module ParserMessages = MclttExtracted.ParserMessages
+open McttExtracted.Entrypoint
+open McttExtracted.Syntax
+module Parser = McttExtracted.Parser
+module ParserMessages = McttExtracted.ParserMessages
 
 (************************************************************)
 (* Formatting helpers *)

driver/PrettyPrinter.mli

@@ -1,6 +1,6 @@
-val format_obj : Format.formatter -> MclttExtracted.Syntax.Cst.obj -> unit
-val format_exp : Format.formatter -> MclttExtracted.Syntax.exp -> unit
-val format_nf : Format.formatter -> MclttExtracted.Syntax.nf -> unit
+val format_obj : Format.formatter -> McttExtracted.Syntax.Cst.obj -> unit
+val format_exp : Format.formatter -> McttExtracted.Syntax.exp -> unit
+val format_nf : Format.formatter -> McttExtracted.Syntax.nf -> unit
 
 val format_main_result :
-  Format.formatter -> MclttExtracted.Entrypoint.main_result -> unit
+  Format.formatter -> McttExtracted.Entrypoint.main_result -> unit

driver/Test.ml

@@ -1,7 +1,7 @@
 (* Unit test cases for parsing *)
 
 open Main
-open MclttExtracted.Entrypoint
+open McttExtracted.Entrypoint
 
 (** Helper definitions *)
 
@@ -100,8 +100,8 @@ let%expect_test "recursion on a natural number that always returns zero is of \
       0 : Nat
   |}]
 
-let%expect_test "simple_nat.mcl works" =
-  let _ = main_of_example "simple_nat.mcl" in
+let%expect_test "simple_nat.mctt works" =
+  let _ = main_of_example "simple_nat.mctt" in
   [%expect
     {|
     Parsed:
@@ -112,8 +112,8 @@ let%expect_test "simple_nat.mcl works" =
       4 : Nat
   |}]
 
-let%expect_test "simple_rec.mcl works" =
-  let _ = main_of_example "simple_rec.mcl" in
+let%expect_test "simple_rec.mctt works" =
+  let _ = main_of_example "simple_rec.mctt" in
   [%expect
     {|
     Parsed:
@@ -129,8 +129,8 @@ let%expect_test "simple_rec.mcl works" =
       : forall (x1 : Nat) -> Nat
   |}]
 
-let%expect_test "pair.mcl works" =
-  let _ = main_of_example "pair.mcl" in
+let%expect_test "pair.mctt works" =
+  let _ = main_of_example "pair.mctt" in
   [%expect
     {|
     Parsed:
@@ -255,8 +255,8 @@ let%expect_test "pair.mcl works" =
       5 : Nat
   |}]
 
-let%expect_test "vector.mcl works" =
-  let _ = main_of_example "vector.mcl" in
+let%expect_test "vector.mctt works" =
+  let _ = main_of_example "vector.mctt" in
   [%expect
     {|
     Parsed:
@@ -463,8 +463,8 @@ let%expect_test "vector.mcl works" =
       7 : Nat
   |}]
 
-let%expect_test "nary.mcl works" =
-  let _ = main_of_example "nary.mcl" in
+let%expect_test "nary.mctt works" =
+  let _ = main_of_example "nary.mctt" in
   [%expect
     {|
     Parsed:
@@ -553,8 +553,8 @@ let%expect_test "nary.mcl works" =
       6 : Nat
   |}]
 
-let%expect_test "simple_let.mcl works" =
-  let _ = main_of_example "simple_let.mcl" in
+let%expect_test "simple_let.mctt works" =
+  let _ = main_of_example "simple_let.mctt" in
   [%expect
     {| 
       Parsed:
@@ -565,8 +565,8 @@ let%expect_test "simple_let.mcl works" =
         1 : Nat      
   |}]
 
-let%expect_test "let_two_vars.mcl works" =
-  let _ = main_of_example "let_two_vars.mcl" in
+let%expect_test "let_two_vars.mctt works" =
+  let _ = main_of_example "let_two_vars.mctt" in
   [%expect
      {|
        Parsed:
@@ -584,8 +584,8 @@ let%expect_test "let_two_vars.mcl works" =
          0 : Nat
   |}]
 
-let%expect_test "let_nary.mcl works" =
-  let _ = main_of_example "let_nary.mcl" in
+let%expect_test "let_nary.mctt works" =
+  let _ = main_of_example "let_nary.mctt" in
   [%expect
      {|
        Parsed:
@@ -675,8 +675,8 @@ let%expect_test "let_nary.mcl works" =
   |}]
 
 
-let%expect_test "let_vector.mcl works" =
-  let _ = main_of_example "let_vector.mcl" in
+let%expect_test "let_vector.mctt works" =
+  let _ = main_of_example "let_vector.mctt" in
   [%expect
     {| 
       Parsed:

driver/dune

@@ -1,21 +1,21 @@
 (include_subdirs no)
 
 (library
- (name Mcltt)
- (public_name mcltt.driver)
+ (name Mctt)
+ (public_name mctt.driver)
  (modules Main Lexer PrettyPrinter Test)
- (libraries MclttExtracted)
+ (libraries McttExtracted)
  (inline_tests
   (deps
-   (glob_files_rec ../examples/*.mcl)))
+   (glob_files_rec ../examples/*.mctt)))
  (preprocess
   (pps ppx_expect)))
 
 (executable
- (name mcltt)
- (public_name mcltt)
- (modules Mcltt)
- (libraries Mcltt))
+ (name mctt)
+ (public_name mctt)
+ (modules Mctt)
+ (libraries Mctt))
 
 (env
  (dev

driver/extracted/dune

@@ -1,5 +1,5 @@
 (library
- (name MclttExtracted)
- (public_name mcltt.extracted))
+ (name McttExtracted)
+ (public_name mctt.extracted))
 
 (documentation)

dune-project

@@ -1,6 +1,6 @@
 (lang dune 3.13)
 (using menhir 2.1)
-(name mcltt)
+(name mctt)
 
 (generate_opam_files)
 
@@ -9,20 +9,20 @@
          "Jason Hu"
          "Junyoung Jang")
 (maintainers "the CompLogic group, McGill University")
-(homepage "https://beluga-lang.github.io/McLTT/")
-(documentation "https://beluga-lang.github.io/McLTT/")
-(source (github Beluga-lang/McLTT))
+(homepage "https://beluga-lang.github.io/McTT/")
+(documentation "https://beluga-lang.github.io/McTT/")
+(source (github Beluga-lang/McTT))
 
 (package
- (name mcltt)
- (synopsis "A Bottom-up Approach to Implementing A Proof Assistant")
- (description "In McLTT, we build a verified, runnable typechecker for Martin-Löf type theory. After
-the accomplishment of this project, we will obtain an executable, to which we can feed
-a program in Martin-Loef type theory, and this executable will check whether this
-program has the specified type. McLTT is novel in that it is implemented in
-Coq. Moreover, we will prove that the typechecking algorithm extracted from Coq is
-sound and complete: a program passes typechecking if and only if it is a well-typed
-program in MLTT. This will be the first verified proof assistant (despite being
+ (name mctt)
+ (synopsis "A Correct-By-Construction Proof Checkers For Type Theories")
+ (description "McTT is a verified, runnable typechecker for Martin-Löf type 
+theory. This project provides an executable, to which we can feed a program 
+in Martin-Löf type theory to check whether this program has the specified type. 
+McTT is novel in that it is implemented and verified in Coq. More specifically, 
+we proved that the typechecking algorithm extracted from Coq is sound and 
+complete: a program passes typechecker if and only if it is a well-typed 
+program in MLTT. This is the first verified proof assistant (despite being 
 elementary) and serves as a basis for future extensions.")
  (depends
   (ocaml (>= "4.14.2"))

scripts/generate_dep.py

@@ -4,7 +4,7 @@
 
 PROJECT_ROOT = Path(__file__).resolve().parents[1]
 THEORIES_ROOT = PROJECT_ROOT / "theories"
-ROOT_MODULE_NAME = "Mcltt"
+ROOT_MODULE_NAME = "Mctt"
 COLORS = {
     "Algorithmic": "darkturquoise",
     "Completeness": "deeppink3",
@@ -57,11 +57,11 @@ def node_of_path(path: str) -> str:
 
     # Handle special case for two main theorems
     # so that printed graph looks better
-    if module_name == "Mcltt.Core.Completeness" or module_name == "Mcltt.Core.Soundness":
+    if module_name == "Mctt.Core.Completeness" or module_name == "Mctt.Core.Soundness":
         result = under_subgraph(f"Core/{node_label}", f""""{module_name}"[label="{node_label}",tooltip="{module_name}",color={color},fillcolor=white];""")
-    elif module_name == "Mcltt.LibTactics":
+    elif module_name == "Mctt.LibTactics":
         result = f"""{{ graph[cluster=false,rank=min]; "{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}]; }}"""
-    elif module_name == "Mcltt.Core.Semantic.Consequences":
+    elif module_name == "Mctt.Core.Semantic.Consequences":
         result = f"""{{ cluster=false; rank=max; "{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}]; }}"""
     else:
         result = f""""{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}];"""
@@ -92,9 +92,9 @@ def data_of_depline(depline: str) -> str:
 def gen_graph() -> str:
     newline = "\n"
     return textwrap.dedent(f"""
-      digraph Mcltt {{
-        graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mcltt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""];
-        node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McLTT/{DOC_BASE}/\\N.html"];
+      digraph Mctt {{
+        graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mctt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""];
+        node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McTT/{DOC_BASE}/\\N.html"];
         {default_subgraph_decl("Algorithmic")}
         {default_subgraph_decl("Core")}
         {core_subgraph_decl("Completeness")}

theories/Algorithmic/Subtyping.v

@@ -1 +1 @@
-From Mcltt.Algorithmic.Subtyping Require Export Definitions Lemmas.
+From Mctt.Algorithmic.Subtyping Require Export Definitions Lemmas.

theories/Algorithmic/Subtyping/Definitions.v

@@ -1,6 +1,6 @@
-From Mcltt.Core Require Import Base.
-From Mcltt.Core.Semantic Require Export NbE.
-From Mcltt.Core.Syntactic Require Export SystemOpt.
+From Mctt.Core Require Import Base.
+From Mctt.Core.Semantic Require Export NbE.
+From Mctt.Core.Syntactic Require Export SystemOpt.
 Import Syntax_Notations.
 
 Reserved Notation "Γ ⊢a A ⊆ A'" (in custom judg at level 80, Γ custom exp, A custom exp, A' custom exp).
@@ -35,4 +35,4 @@ Inductive alg_subtyping : ctx -> typ -> typ -> Prop :=
 where "Γ ⊢a A ⊆ B" := (alg_subtyping Γ A B) (in custom judg) : type_scope.
 
 #[export]
-Hint Constructors alg_subtyping_nf alg_subtyping: mcltt.
+Hint Constructors alg_subtyping_nf alg_subtyping: mctt.