Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Roqc/dev/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 1 kB image not shown  

Quellcode-Bibliothek dune-dbg.in   Sprache: unbekannt

 
#!/usr/bin/env bash
# Run in a proper install dune env.

opts=()
while [[ $# -gt 0 ]]; do
    case $1 in
        -emacs)
            shift
            opts+=("-emacs")
            ;;
        -I)
          shift
          opts+=("-I" "$1")
          shift
          ;;
        coqchk)
            shift
            exe=_build/default/checker/coqchk.bc
            opts+=($(ocamlfind query -recursive -i-format rocq-runtime.checklib))
            break
            ;;
        rocqide)
            shift
            exe=_build/default/ide/rocqide/rocqide_main.bc
            break
            ;;
        coqc)
            shift
            exe="_build/default/topbin/rocqworker.bc --kind=compile"
            break
            ;;
        coqtop)
            shift
            exe=_build/default/topbin/coqtop_byte_bin.bc
            break
            ;;
        coqnative)
            shift
            exe=_build/default/topbin/rocqnative.bc
            break
            ;;
        *)
            echo "usage: dune exec -- dev/dune-dbg [-emacs] {coqchk|rocqide|coqc|coqtop|coqdep|coqnative} coqargs"
            exit 1
            ;;
    esac
done

export ROCQLIB=$PWD/_build/install/default/lib/coq
ocamldebug "${opts[@]}" $(ocamlfind query -recursive -i-format rocq-runtime.dev) $(ocamlfind query -i-format -descendants rocq-runtime.vernac) -I +threads -I dev $exe "$@"

[ 0.15Quellennavigators  Projekt   ]