mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-16 14:57:13 +03:00
Lots of documentation
This commit is contained in:
Denis Merigoux
parent
01b1fdf0b6
commit
606b148c74
@ -14,53 +14,21 @@ by contributing, you disclaim all copyright interests in favor of Inria.
|
||||
Both the code for the compiler and the examples in this repository are
|
||||
distributed under the Apache2 license.
|
||||
|
||||
## Writing Catala examples
|
||||
|
||||
### Setting up the machinery
|
||||
|
||||
This section describes what to do to setup a working directory for a new Catala example, as well as the development cycle. Let us suppose that you want to create a new example named `foo`.
|
||||
|
||||
First, follow the instructions of [the installation readme](INSTALL.md) to get the compiler up and working up to `make build`. You can also set up the syntax highlighting for your editor.
|
||||
|
||||
Then, create the directory `examples/foo`. In there, create a master source file `foo.catala` that will be the root of your Catala program. You can then start programming in `foo.catala`, or split up your example into multiple files. In the later case, `foo.catala` must only contain something like this:
|
||||
|
||||
```
|
||||
@@Master file@@
|
||||
|
||||
@@Include: bar.catala@@
|
||||
```
|
||||
|
||||
where `examples/bar.catala` is another source file containing code for your example. Make sure you start by including some content in the source files, like
|
||||
|
||||
```
|
||||
Hello, world!
|
||||
```
|
||||
|
||||
Now let's build the example, create a `Makefile` with the following contents:
|
||||
|
||||
```Makefile
|
||||
CATALA_LANG=en # or fr if your source code is in French
|
||||
SRC=foo.catala
|
||||
|
||||
include ../Makefile.common
|
||||
```
|
||||
|
||||
The `include` creates automatically all the targets you will need for your example. For instance, after making sure the compiler is built, you can launch
|
||||
|
||||
```
|
||||
make -C examples/foo foo.tex
|
||||
```
|
||||
|
||||
from the repository root to create the LaTeX weaving output of your source program. `Hello, world!` should appear in there.
|
||||
|
||||
Finally, please add a rule for your example in the repository root `Makefile` in the section "Examples-related rules", following the pattern for other examples. This will ensure that
|
||||
your example is built every time the compiler is modified; if a change in the compiler breaks your example, the authors will be notified and find a solution.
|
||||
|
||||
### Writing Catala code
|
||||
|
||||
Let us now present the typical Catala workflow. First, you need to locate the legislative text that you want to use as a reference. Then, simply copy-paste the text into your source file.
|
||||
Before writing Catala code, please read the
|
||||
[tutorial](https://catala-lang.org/en/examples/tutorial). You can run the
|
||||
programs of the tutorial yourself by following the instruction in the
|
||||
[README of the `examples` directory](examples/README.md). Then, it is suggested
|
||||
that you create a new example directory again according to the instructions of
|
||||
this README.
|
||||
|
||||
First you will have to format the copy-pasted text using Catala headings and articles markers:
|
||||
Let us now present the typical Catala workflow. First, you need to locate
|
||||
the legislative text that you want to use as a reference. Then, simply
|
||||
copy-paste the text into your source file.
|
||||
|
||||
First you will have to format the copy-pasted text using Catala headings
|
||||
and articles markers:
|
||||
|
||||
```
|
||||
@@Heading@@
|
||||
@ -70,14 +38,18 @@ First you will have to format the copy-pasted text using Catala headings and art
|
||||
@Legislative atom@
|
||||
```
|
||||
|
||||
Please look at the code of other examples to see how to format things properly. While formatting the text, don't forget regularly to try and parse your example using for instance
|
||||
Please look at the code of other examples to see how to format things properly.
|
||||
While formatting the text, don't forget regularly to try and parse your example
|
||||
using for instance
|
||||
|
||||
|
||||
```
|
||||
make -C examples/foo foo.tex
|
||||
```
|
||||
|
||||
to see if you've made any syntax errors. Once the text formatting is done, you can start to annotate each legislative atom (article, provision, etc.) with some Catala code. To open up a code section in Catala, simply use
|
||||
to see if you've made any syntax errors. Once the text formatting is done, you
|
||||
can start to annotate each legislative atom (article, provision, etc.) with
|
||||
some Catala code. To open up a code section in Catala, simply use
|
||||
|
||||
```
|
||||
/*
|
||||
@ -87,7 +59,9 @@ scope Foo:
|
||||
*/
|
||||
```
|
||||
|
||||
While all the code sections are equivalent in terms of execution, you can mark some as "metadata" so that they are printed differently on lawyer-facing documents. Here's how it works:
|
||||
While all the code sections are equivalent in terms of execution, you can
|
||||
mark some as "metadata" so that they are printed differently on lawyer-facing
|
||||
documents. Here's how it works:
|
||||
|
||||
```
|
||||
@@Begin metadata@@ # @@Début métadonnées@@ en français
|
||||
@ -101,11 +75,17 @@ declaration structure FooBar:
|
||||
@@End metadata@@ # @@Fin métadonnées@@ en français
|
||||
```
|
||||
|
||||
Again, make sure to regularly check that your example is parsing correctly. The error message from the compiler should help you debug the syntax if need be.
|
||||
Again, make sure to regularly check that your example is parsing correctly. The error message from the compiler should help you debug the syntax if need be. You can also
|
||||
live-test the programs you wrote by feeding them to the interpreter
|
||||
(see the [README of the `examples` directory](examples/README.md)); this will
|
||||
also type-check the programs, which is useful for debugging them.
|
||||
|
||||
## Working on the compiler
|
||||
|
||||
The Catala compiler is a standard dune-managed OCaml project. You can look at the [online OCaml documentation](https://catala-lang.org/ocaml_docs/) for the different modules' interfaces.
|
||||
The Catala compiler is a standard dune-managed OCaml project.
|
||||
You can look at the
|
||||
[online OCaml documentation](https://catala-lang.org/ocaml_docs/) for the
|
||||
different modules' interfaces as well as high-level architecture documentation.
|
||||
|
||||
## Internationalization
|
||||
|
||||
|
||||
@ -75,10 +75,6 @@ You will need the `man2html` executable to generate the HTML versions of the man
|
||||
pages, as well as the `rsync` executable to transfer files (preferred to `cp`)
|
||||
because it also works with a remote server.
|
||||
|
||||
## Usage
|
||||
|
||||
Use `catala --help` to get more information about the command line options available.
|
||||
|
||||
## Syntax highlighting
|
||||
|
||||
The Catala language also comes with syntax highlighting to
|
||||
|
||||
4
Makefile
4
Makefile
@ -136,10 +136,10 @@ literate_examples: literate_allocations_familiales literate_code_general_impots
|
||||
.FORCE:
|
||||
|
||||
test_suite: .FORCE
|
||||
@$(MAKE) --no-print-directory -C tests
|
||||
@$(MAKE) --no-print-directory -C tests pass_tests
|
||||
|
||||
test_examples: .FORCE
|
||||
@$(MAKE) --no-print-directory -C examples test_examples
|
||||
@$(MAKE) --no-print-directory -C examples tests
|
||||
|
||||
tests: test_suite test_examples
|
||||
|
||||
|
||||
14
README.md
14
README.md
@ -47,10 +47,15 @@ The Catala language is the only programming language to our knowledge that
|
||||
embeds default logic as a first-class feature, which is why it is the only
|
||||
language perfectly adapted to literate legislative programming.
|
||||
|
||||
## Installation
|
||||
## Building and installation
|
||||
|
||||
See [the dedicated readme](INSTALL.md).
|
||||
|
||||
## Usage
|
||||
|
||||
Use `catala --help` to get more information about the command line
|
||||
options available.
|
||||
|
||||
## Examples
|
||||
|
||||
See [the dedicated readme](examples/README.md).
|
||||
@ -86,12 +91,7 @@ The library is released under the [Apache license (version 2)](LICENSE.txt).
|
||||
|
||||
Catala is a research project from Inria, the French National
|
||||
Research Institute for Computer Science. The compiler is yet
|
||||
unstable and lacks some of its features. Currently, here is the list
|
||||
of existing features:
|
||||
|
||||
* Literate programming output to HTML or LaTeX
|
||||
* Typechecker and interpreter for most of the language
|
||||
|
||||
unstable and lacks some of its features.
|
||||
|
||||
## Pierre Catala
|
||||
|
||||
|
||||
10
doc/formalization/README.md
Normal file
10
doc/formalization/README.md
Normal file
@ -0,0 +1,10 @@
|
||||
# The Catala formalization
|
||||
|
||||
This folder contains the LaTeX sources of the document describing the
|
||||
formalization the Catala programming language. To build the PDF output,
|
||||
simply invoke:
|
||||
|
||||
make formalization
|
||||
|
||||
The directory also contains the F* sources of the proof of type soundness
|
||||
of this formalization.
|
||||
@ -18,7 +18,7 @@
|
||||
> /dev/null || { echo "[FAIL $@]"; exit 1; }
|
||||
@echo "[PASS $@]"
|
||||
|
||||
TEST_FILES=$(wildcard */tests/*.catala*)
|
||||
TEST_FILES?=$(wildcard */tests/*.catala*)
|
||||
|
||||
TEST_FILES_SCOPES_EN=$(foreach TEST_FILE,$(TEST_FILES),\
|
||||
$(foreach TEST_SCOPE,\
|
||||
@ -34,6 +34,6 @@ TEST_FILES_SCOPES_FR=$(foreach TEST_FILE,$(TEST_FILES),\
|
||||
) \
|
||||
)
|
||||
|
||||
test_examples: $(TEST_FILES_SCOPES_EN) $(TEST_FILES_SCOPES_FR)
|
||||
tests: $(TEST_FILES_SCOPES_EN) $(TEST_FILES_SCOPES_FR)
|
||||
|
||||
.FORCE:
|
||||
@ -12,10 +12,6 @@ CATALA=dune exec --no-print-director ../../src/catala.exe -- $(CATALA_OPTS) --la
|
||||
LEGIFRANCE_CATALA=dune exec ../../src/legifrance_catala.exe --
|
||||
|
||||
CATALA_EXE=../../_build/default/src/catala.exe
|
||||
LEGIFRANCE_CATALA_EXE=../../_build/default/src/legifrance_catala.exe
|
||||
|
||||
CLIENT_ID?=$(shell cat ../../legifrance_oauth_id.txt)
|
||||
CLIENT_SECRET?=$(shell cat ../../legifrance_oauth_secret.txt)
|
||||
|
||||
ifeq ($(CATALA_LANG),fr)
|
||||
PYGMENTIZE=$(PYGMENTIZE_FR)
|
||||
@ -51,9 +47,6 @@ endif
|
||||
HTML \
|
||||
$<
|
||||
|
||||
%.expired: %.catala_$(CATALA_LANG) $(CATALA_EXE) $(LEGIFRANCE_CATALA_EXE)
|
||||
$(LEGIFRANCE_CATALA) $< $(CLIENT_ID) $(CLIENT_SECRET)
|
||||
|
||||
%.pdf: %.tex
|
||||
cd $(@D) && $(LATEXMK) -g -pdf -halt-on-error -shell-escape $(%F)
|
||||
|
||||
122
examples/README.md
Normal file
122
examples/README.md
Normal file
@ -0,0 +1,122 @@
|
||||
# Catala examples
|
||||
|
||||
This directory contains examples of Catala programs. It is highly recommended
|
||||
to locate your own Catala programs in this directory, since programs in this
|
||||
directory will receive first-class support during the alpha and beta stage
|
||||
of the Catala programming language development.
|
||||
|
||||
## List of examples
|
||||
|
||||
* `allocations_familiales/`: computation of the French family benefits, based
|
||||
on the _Code de la sécurité sociale_. This case study is the biggest and
|
||||
most ambitious for Catala so far.
|
||||
* `code_general_impots/`: computation of the French income tax, based on the
|
||||
_Code général des impôts_. Currently, there are only stubs of program.
|
||||
* `tutorial/`: Catala language tutorial for developers of tech-savvy lawyers.
|
||||
The tutorial is written like a piece of legislation that gets annotated by
|
||||
Catala snippets.
|
||||
* `us_tax_code/`: contains the Catala formalization of several sections of the
|
||||
US Tax Code.
|
||||
|
||||
## Building and running examples
|
||||
|
||||
Building and running examples is done via Makefiles. Each example directory
|
||||
contains its own Makefile, which includes `Makefile.common.mk`. This common
|
||||
Makefiles defines a list of targets that call the Catala compiler with the
|
||||
right options. Each of these targers can be called from the root of the
|
||||
repository with:
|
||||
|
||||
make -C examples/<directory of example> <name of target>
|
||||
|
||||
The `<name of target>` can be replaced with the following (we assume an example
|
||||
file `examples/foo/foo.catala_en`) list.
|
||||
|
||||
* `foo.tex`: builds the LaTeX literate programming output from the Catala program
|
||||
* `foo.pdf`: compiles `foo.tex` using `latexmk`
|
||||
* `foo.html`: builds the HTML literate programming output from the Catala program
|
||||
* `foo.run`: interprets the Catala program contained in `foo.catala_en`. Note
|
||||
that you have to pass in the scope that you want to interpret via the `SCOPE`
|
||||
Makefile variable (`SCOPE=FooScope make -C examples/foo foo.run`).
|
||||
|
||||
When invoking any of these targets, additional options to the Catala compiler
|
||||
can be passed using the `CATALA_OPTS` Makefile variable.
|
||||
|
||||
## Testing examples
|
||||
|
||||
Unit testing is important, and we encourage Catala developers to write lots
|
||||
of tests for their programs. Again, the Makefile system provides a way to
|
||||
collect tests into a regression test suite.
|
||||
|
||||
In order to enjoy the benefits of this system, you have to create a `tests/`
|
||||
directory in your examples directory, for instance `examples/foo/tests`. Then,
|
||||
create a test file `foo_tests.catala_en` inside that directory.
|
||||
|
||||
Inside `foo_tests.catala_en`, declare one ore more test scopes. It is assumed
|
||||
that all these scopes should execute correctly. Include the program scope you
|
||||
want to test and use assertions to provide the expected values of your test.
|
||||
See existing tests in examples directory for more information.
|
||||
|
||||
Once your tests are written, then will automatically be added to the regression
|
||||
suite executed using
|
||||
|
||||
make -C examples tests
|
||||
|
||||
You can isolate a part of the regression suite by invoking:
|
||||
|
||||
TEST_FILES=examples/tests/foo/foo_tests.catala_en make -C examples tests
|
||||
|
||||
## Adding an example
|
||||
|
||||
This section describes what to do to setup a working directory for a new Catala
|
||||
example, as well as the development cycle. Let us suppose that you want to
|
||||
create a new example named `foo`.
|
||||
|
||||
First, follow the instructions of [the installation readme](../INSTALL.md) to
|
||||
get the compiler up and working up to `make build`. You can also set up the
|
||||
syntax highlighting for your editor.
|
||||
|
||||
Then, create the directory `examples/foo`. In there, create a master source
|
||||
file `foo.catala` that will be the root of your Catala program.
|
||||
You can then start programming in `foo.catala`, or split up your example
|
||||
into multiple files. In the later case, `foo.catala` must only contain
|
||||
something like this:
|
||||
|
||||
```
|
||||
@@Master file@@
|
||||
|
||||
@@Include: bar.catala@@
|
||||
```
|
||||
|
||||
where `examples/bar.catala` is another source file containing code for your
|
||||
example. Make sure you start by including some content in the source files,
|
||||
like
|
||||
|
||||
```
|
||||
Hello, world!
|
||||
```
|
||||
|
||||
To build and run the example, create a `Makefile` in `foo/`
|
||||
with the following contents:
|
||||
|
||||
```Makefile
|
||||
CATALA_LANG=en # or fr if your source code is in French
|
||||
SRC=foo.catala
|
||||
|
||||
include ../Makefile.common.mk
|
||||
```
|
||||
|
||||
The `include` creates automatically all the targets you will need for your example. For instance, after making sure the compiler is built, you can launch
|
||||
|
||||
```
|
||||
make -C examples/foo foo.tex
|
||||
```
|
||||
|
||||
from the repository root to create the LaTeX weaving output of your source
|
||||
program. `Hello, world!` should appear in `examples/foo/foo.tex`.
|
||||
|
||||
Finally, please add a rule for your example in the repository root
|
||||
`Makefile` in the section "Examples-related rules", following the pattern
|
||||
for other examples. This will ensure that your example is built every
|
||||
time the compiler is modified; if a change in the compiler breaks your example,
|
||||
the authors will be notified and find a solution.
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
CATALA_LANG=fr
|
||||
SRC=allocations_familiales.catala_fr
|
||||
|
||||
include ../Makefile.common
|
||||
include ../Makefile.common.mk
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
CATALA_LANG=fr
|
||||
SRC=code_general_impots.catala_fr
|
||||
|
||||
include ../Makefile.common
|
||||
include ../Makefile.common.mk
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
CATALA_LANG=en
|
||||
SRC=tutorial_en.catala_en
|
||||
|
||||
include ../Makefile.common
|
||||
include ../Makefile.common.mk
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
CATALA_LANG=en
|
||||
SRC=us_tax_code.catala_en
|
||||
|
||||
include ../Makefile.common
|
||||
include ../Makefile.common.mk
|
||||
|
||||
Loading…
Reference in New Issue
Block a user