Mentions légales du service

Skip to content
  • Rehan MALAK's avatar
    This is an experimental branch to play with Ptree's · e53e78b4
    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