README

HOW TO SET UP YOUR ENVIRONMENT

1. Download and Unpack
1.1. Clone CompCert [optional, if you plan to use clightgen]
1.2. Clone VST
1.3. Clone RamifyCoq
1.4. Your life will be a bit easier if these three are in sibling directories
     named CompCert, VST, and RamifyCoq. 

2. Build CompCert [optional, if you plan to use clightgen]
In CompCert/
2.1. make clean
2.2 ./configure -clightgen {your_operating_system}  
    see CompCert/configure for the OS options you have
2.2. make -j7

2. Build VST
In VST/
2.1. make clean
2.2. make -j7

3. Build RamifyCoq
In RamifyCoq/
3.1. Create a file CONFIGURE in your RamifyCoq folder with (only) these two lines in it:
COMPCERT_DIR=../VST/compcert
VST_DIR=../VST 
3.2. make clean
3.3. make -j7 

4. Set up your ProofGeneral Environment [optional]
4.1. Install ProofGeneral in your computer.
4.2. Add ProofGeneral into your emacs setting files.
4.3. Add these two paragraghs into your emacs setting files.
(custom-set-variables '(coq-prog-args '(
"-R" "[Your CompCert Folder]" "-as" "compcert" 
"-R" "[Your VST Folder]" "-as" "VST" 
"-R" "[Your RamifyCoq Folder]" "-as" "RamifyCoq"))) 

(setq coq-load-path '(("[Your CompCert Folder]" "compcert")
                      ("[Your VST Folder]" "VST")
                      ("[Your RamifyCoq Folder]" "RamifyCoq")))

5. You can play with RamifyCoq as it stands.

6. Developing Inside RamifyCoq
6.1. Write your newfile.c inside RamifyCoq.
6.2. {path_to_compcert}/CompCert/clightgen -DCOMPCERT -normalize -isystem . newfile.c
6.3. Open RamifyCoq/Makefile and add newfile.v to the list of sources
6.4. In RamifyCoq/, make depend (this is for every time you edit the makefile)
6.5. In RamifyCoq/, make {path_to_newfile.c}/newfile.vo (note the .vo)
6.6. Create verif_newfile.v. Something like "Require Import RamifyCoq.path.path.newfile." will now work.
6.7. Don't forget to check that your VCS is tracking these files you just created.