Mentions légales du service

Skip to content
Snippets Groups Projects
Forked from Why3 / why3
Source project has a limited visibility.
Rehan Malak's avatar
Rehan MALAK authored
0) opam install ppx_optcomp

1) build why3 with --enable-local :

git clean -dffx && ./autogen.sh && ./configure --enable-local && make -j8

2) play with ptree's api

cd examples/use_api
make

3) why3_ptree is a program parsing a *.mlw file that returns the complete ptree (list of modules) and then print the ptree in debug mode and with a pretty printer :

  ./why3_ptree ../examples/logic/real.why

In particular, it has a ptree ast debug printer

  Why3ml_pp.Output_ast.print_mlw_file

and a ptree pretty printer

  Why3ml_pp.Output_mlw.print_mlw_file
e53e78b4
History
Name Last commit Last update
..