Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Back merge #265

Closed
wants to merge 6 commits into from
Closed
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Change McLTT into McTT (#262)
Ailrun authored Nov 16, 2024
commit 7d870396b188cb18e7b3f22d7805296e0c5b7e2f
6 changes: 3 additions & 3 deletions .github/workflows/ci_build.yaml
Original file line number Diff line number Diff line change
@@ -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: A Bottom-up Approach to Implementing A Proof Assistant' -t html --css styling.css -o html/index.html
fi
endGroup
startGroup "Run inline tests"
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
@@ -76,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:
2 changes: 1 addition & 1 deletion assets/include.html
Original file line number Diff line number Diff line change
@@ -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>`);
6 changes: 3 additions & 3 deletions driver/Lexer.mli
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion driver/Lexer.mll
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
open Lexing
open MclttExtracted.Parser
open McttExtracted.Parser

let get_range lexbuf = (lexbuf.lex_start_p, lexbuf.lex_curr_p)

4 changes: 2 additions & 2 deletions driver/Main.ml
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion driver/Mcltt.ml → driver/Mctt.ml
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
open Mcltt.Main
open Mctt.Main

let () =
if Array.length Sys.argv <> 2
8 changes: 4 additions & 4 deletions driver/PrettyPrinter.ml
Original file line number Diff line number Diff line change
@@ -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 *)
8 changes: 4 additions & 4 deletions driver/PrettyPrinter.mli
Original file line number Diff line number Diff line change
@@ -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
38 changes: 19 additions & 19 deletions driver/Test.ml
Original file line number Diff line number Diff line change
@@ -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:
16 changes: 8 additions & 8 deletions driver/dune
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions driver/extracted/dune
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(library
(name MclttExtracted)
(public_name mcltt.extracted))
(name McttExtracted)
(public_name mctt.extracted))

(documentation)
26 changes: 13 additions & 13 deletions dune-project
Original file line number Diff line number Diff line change
@@ -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"))
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
14 changes: 7 additions & 7 deletions scripts/generate_dep.py
Original file line number Diff line number Diff line change
@@ -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")}
2 changes: 1 addition & 1 deletion theories/Algorithmic/Subtyping.v
Original file line number Diff line number Diff line change
@@ -1 +1 @@
From Mcltt.Algorithmic.Subtyping Require Export Definitions Lemmas.
From Mctt.Algorithmic.Subtyping Require Export Definitions Lemmas.
8 changes: 4 additions & 4 deletions theories/Algorithmic/Subtyping/Definitions.v
Original file line number Diff line number Diff line change
@@ -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.
14 changes: 7 additions & 7 deletions theories/Algorithmic/Subtyping/Lemmas.v
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
From Mcltt Require Import LibTactics.
From Mcltt.Algorithmic.Subtyping Require Import Definitions.
From Mcltt.Core Require Import Base Soundness.
From Mcltt.Core.Syntactic Require Import SystemOpt.
From Mcltt.Core.Completeness.Consequences Require Import Rules.
From Mctt Require Import LibTactics.
From Mctt.Algorithmic.Subtyping Require Import Definitions.
From Mctt.Core Require Import Base Soundness.
From Mctt.Core.Syntactic Require Import SystemOpt.
From Mctt.Core.Completeness.Consequences Require Import Rules.
Import Syntax_Notations.

#[local]
@@ -61,7 +61,7 @@ Proof.
Qed.

#[local]
Hint Resolve alg_subtyping_nf_trans alg_subtyping_nf_refl : mcltt.
Hint Resolve alg_subtyping_nf_trans alg_subtyping_nf_refl : mctt.

Lemma alg_subtyping_trans : forall Γ A0 A1 A2,
{{ Γ ⊢a A0 ⊆ A1 }} ->
@@ -74,7 +74,7 @@ Proof.
Qed.

#[local]
Hint Resolve alg_subtyping_trans : mcltt.
Hint Resolve alg_subtyping_trans : mctt.

Lemma alg_subtyping_complete : forall Γ A B,
{{ Γ ⊢ A ⊆ B }} ->
2 changes: 1 addition & 1 deletion theories/Algorithmic/Typing.v
Original file line number Diff line number Diff line change
@@ -1 +1 @@
From Mcltt.Algorithmic.Typing Require Export Definitions Lemmas.
From Mctt.Algorithmic.Typing Require Export Definitions Lemmas.
6 changes: 3 additions & 3 deletions theories/Algorithmic/Typing/Definitions.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From Mcltt.Algorithmic.Subtyping Require Export Definitions.
From Mcltt.Core Require Import Base.
From Mctt.Algorithmic.Subtyping Require Export Definitions.
From Mctt.Core Require Import Base.
Import Domain_Notations.

Reserved Notation "Γ '⊢a' M ⟹ A" (in custom judg at level 80, Γ custom exp, M custom exp, A custom nf).
@@ -51,7 +51,7 @@ with alg_type_infer : ctx -> nf -> exp -> Prop :=
where "Γ '⊢a' M ⟹ A" := (alg_type_infer Γ A M) (in custom judg) : type_scope.

#[export]
Hint Constructors alg_type_check alg_type_infer : mcltt.
Hint Constructors alg_type_check alg_type_infer : mctt.

Scheme alg_type_check_mut_ind := Induction for alg_type_check Sort Prop
with alg_type_infer_mut_ind := Induction for alg_type_infer Sort Prop.
Loading