Skip to content

Compiling CoqTL

Zheng Cheng edited this page Jul 17, 2020 · 7 revisions

Prequisite

  • Install Coq
    • type in command-line: coqc --version to verify Coq installation, please make sure Coq version is at least 8.11.1

Compile

  • get a copy of CoqTL:
    • git clone https://github.com/atlanmod/CoqTL.git
  • navigate to the root of the CoqTL language:
    1. cd CoqTL
    2. cd fr.inria.atlanmod.coqtl.coq
  • switch to the branch of interest:
    • flat-syntax-parametric branch corresponds to MODELS'2020 submission, which certifies engine for proof preservation
      • git switch flat-syntax-parametric
  • compile the CoqTL language:
    1. coq_makefile -f _CoqProject -o Makefile
    2. make
  • Ready to use.

Misc

  • The dependencies among CoqTL files is managed by _CoqProject in the root of the CoqTL language.
  • This page serves both for WINDOWS and LINUX users. If encounter trouble, please send an ISSUE.
Clone this wiki locally