diff options
| -rw-r--r-- | Makefile | 30 | ||||
| -rw-r--r-- | config/Makefile.template | 4 | ||||
| -rwxr-xr-x | configure | 34 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 95 | ||||
| -rw-r--r-- | scripts/coqc.ml4 | 7 | ||||
| -rw-r--r-- | scripts/coqmktop.ml | 17 |
6 files changed, 99 insertions, 88 deletions
@@ -129,10 +129,14 @@ CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx) COQMKTOP=scripts/coqmktop COQC=scripts/coqc -world: $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt states theories contrib tools +BESTCOQTOP=coqtop.$(BEST) +COQBINARIES= $(COQMKTOP) $(COQC) coqtop.byte $(BESTCOQTOP) + +world: $(COQBINARIES) states theories contrib tools coqtop.opt: $(COQMKTOP) $(CMX) - $(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop.opt + $(COQMKTOP) -opt $(OPTFLAGS) -o coqtop.opt + strip ./coqtop.opt coqtop.byte: $(COQMKTOP) $(CMO) Makefile $(COQMKTOP) -top $(BYTEFLAGS) -o coqtop.byte @@ -155,6 +159,7 @@ scripts/tolink.ml: Makefile echo "let tactics = \""$(TACTICS)"\"" >> $@ echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@ echo "let hightactics = \""$(HIGHTACTICS)"\"" >> $@ + echo "let contrib = \""$(CONTRIB)"\"" >> $@ beforedepend:: scripts/tolink.ml @@ -162,7 +167,7 @@ beforedepend:: scripts/tolink.ml COQCCMO=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo -$(COQC): $(COQCCMO) +$(COQC): $(COQCCMO) coqtop.byte coqtop.$(BEST) $(OCAMLC) $(BYTEFLAGS) -o $(COQC) -custom unix.cma $(COQCCMO) \ $(OSDEPLIBS) @@ -191,8 +196,8 @@ states: states/barestate.coq states/initial.coq SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v syntax/PPTactic.v -states/barestate.coq: $(SYNTAXPP) coqtop.byte - ./coqtop.byte -q -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq +states/barestate.coq: $(SYNTAXPP) $(BESTCOQTOP) + ./$(BESTCOQTOP) -q -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/DatatypesSyntax.vo theories/Init/Prelude.vo \ @@ -201,16 +206,20 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic_Type.vo theories/Init/Wf.vo \ theories/Init/Logic_TypeSyntax.vo +theories/Init/%.vo: $(COQC) theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) -q -I theories/Init -is states/barestate.coq $< +init: $(INITVO) + TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo +tactics/%.vo: $(COQC) tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) -q -I tactics -is states/barestate.coq $< -states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) - ./coqtop.byte -q -batch -silent -is states/barestate.coq -I tactics -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq +states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) $(BESTCOQTOP) + ./$(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq clean:: rm -f states/barestate.coq states/initial.coq @@ -224,8 +233,8 @@ ARITHVO=theories/Arith/Arith.vo theories/Arith/Gt.vo \ theories/Arith/Between.vo theories/Arith/Le.vo \ theories/Arith/Compare.vo theories/Arith/Lt.vo \ theories/Arith/Compare_dec.vo theories/Arith/Min.vo \ - theories/Arith/Div2.vo theories/Arith/Minus.vo \ - theories/Arith/Mult.vo theories/Arith/Even.vo \ + theories/Arith/Div2.vo theories/Arith/Minus.vo \ + theories/Arith/Mult.vo theories/Arith/Even.vo \ theories/Arith/EqNat.vo theories/Arith/Peano_dec.vo \ theories/Arith/Euclid_def.vo theories/Arith/Plus.vo \ theories/Arith/Euclid_proof.vo theories/Arith/Wf_nat.vo \ @@ -245,7 +254,6 @@ $(THEORIESVO): states/initial.coq theories: $(THEORIESVO) -init: $(INITVO) logic: $(LOGICVO) arith: $(ARITHVO) bool: $(BOOLVO) @@ -471,7 +479,7 @@ toplevel/mltop.cmx: toplevel/mltop.ml4 $(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $< .v.vo: - $(COQC) $(COQINCLUDES) -q $< + $(COQC) -q -$(BEST) $(COQINCLUDES) $< .el.elc: echo "(setq load-path (cons \".\" load-path))" > $*.compile diff --git a/config/Makefile.template b/config/Makefile.template index 6ae9ca84a..52c054372 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -59,8 +59,8 @@ CAMLDEBUG=COQDEBUGFLAG # Compilation profile flag CAMLTIMEPROF=COQPROFILEFLAG -# Compilation of tools: bytecode (=byte) or native (=opt) -COQTOOLS=COQTOOLSFLAG +# The best compiler: native (=opt) or bytecode (=byte) if no native compiler +BEST=BESTCOMPILER # For Camlp4 use P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing @@ -25,7 +25,7 @@ bytecamlc=ocamlc nativecamlc=ocamlopt coq_debug_flag= coq_profile_flag= -byte_opt_tools=opt +best_compiler=opt local=false bindir_spec=no @@ -81,8 +81,7 @@ while : ; do shift;; -opt|--opt) bytecamlc=ocamlc.opt nativecamlc=ocamlopt.opt;; - -opt-tools|-opttools|--opttools|--opt-tools) byte_opt_tools=opt;; - -byte-tools|-bytetools|--bytetools|--byte-tools) byte_opt_tools=byte;; + -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;; -debug|--debug) coq_debug_flag=-g;; -profile|--profile) coq_profile_flag=-p;; *) echo "Unknown option \"$1\"." 1>&2; exit 2;; @@ -266,9 +265,9 @@ CAMLBIN=`dirname $CAMLC` CAMLVERSION=`$CAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` case $CAMLVERSION in - 1.*|2.00) + 1.*|2.*) echo "Your version of Objective-Caml is $CAMLVERSION." - echo "You need Objective-Caml 2.01 or later !" + echo "You need Objective-Caml 3.00 or later !" echo "Configuration script failed!" exit 1;; ?*) echo "You have Objective-Caml $CAMLVERSION. Good!";; @@ -278,12 +277,19 @@ case $CAMLVERSION in exit 1;; esac -# do we have a native compiler: test of ocamlopt - -CAMLOPT=`which ocamlopt` -case $CAMLOPT in - "") byte_opt_tools=byte;; -esac +# do we have a native compiler: test of ocamlopt and its version + +if [ $best_compiler = "opt" ] ; then + CAMLOPT=`which $nativecamlc` + case $CAMLOPT in + "") best_compiler=byte + echo "You have only bytecode compilation.";; + *) CAMLOPTVERSION=`$CAMLOPT -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` + if [ $CAMLOPTVERSION != $CAMLVERSION ] ; then \ + echo "native and bytecode compilers do not have the same version!"; fi + echo "You have native-code compilation. Good!" + esac +fi # For Dynlink @@ -293,7 +299,7 @@ CAMLLIB=`ocamlc -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' ` CAMLP4=`which camlp4` case $CAMLP4 in - "") echo "camlp4 is not present in your path !" + "") echo "camlp4 is not present in your path!" echo "Give me manually the path to the camlp4 executable [/usr/local/bin by default]: " read CAMLP4 @@ -387,7 +393,7 @@ case $ARCH in -e "s|OSKIND|$OSTYPE|" \ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ - -e "s|COQTOOLSFLAG|$byte_opt_tools|" \ + -e "s|BESTCOMPILER|$best_compiler|" \ -e "s|EXECUTEEXTENSION|$EXE|" \ -e "s|BYTECAMLC|$bytecamlc|" \ -e "s|NATIVECAMLC|$nativecamlc|" \ @@ -412,7 +418,7 @@ case $ARCH in -e "s|OSKIND|$OSTYPE|" \ -e "s|COQDEBUGFLAG|$coq_debug_flag|" \ -e "s|COQPROFILEFLAG|$coq_profile_flag|" \ - -e "s|COQTOOLSFLAG|$byte_opt_tools|" \ + -e "s|BESTCOMPILER|$best_compiler|" \ -e "s|EXECUTEEXTENSION|$EXE|" \ -e "s|BYTECAMLC|$bytecamlc|" \ -e "s|NATIVECAMLC|$nativecamlc|" \ diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 034389549..bd7ff32a7 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -32,27 +32,27 @@ type value= |VArg of tactic_arg |VFun of (string*value) list*string option list*Coqast.t |VVoid - |VRec of value ref;; + |VRec of value ref (*Gives the identifier corresponding to an Identifier tactic_arg*) let id_of_Identifier=function Identifier id -> id |_ -> - anomalylabstrm "id_of_IDENTIFIER" [<'sTR "Not an IDENTIFIER tactic_arg">];; + anomalylabstrm "id_of_IDENTIFIER" [<'sTR "Not an IDENTIFIER tactic_arg">] (*Gives the constr corresponding to a Constr tactic_arg*) let constr_of_Constr=function Constr c -> c - |_ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">];; + |_ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">] (*Signature for interpretation: val_interp and interpretation functions*) type interp_sign= evar_declarations*Environ.env*(string*value) list*(int*constr) list* - goal sigma option;; + goal sigma option (*Table of interpretation functions*) let interp_tab= - (Hashtbl.create 17:(string,interp_sign->Coqast.t->value) Hashtbl.t);; + (Hashtbl.create 17:(string,interp_sign->Coqast.t->value) Hashtbl.t) (*Adds an interpretation function*) let interp_add (ast_typ,interp_fun)= @@ -62,37 +62,38 @@ let interp_add (ast_typ,interp_fun)= Failure _ -> errorlabstrm "interp_add" [<'sTR "Cannot add the interpretation function for "; 'sTR ast_typ; 'sTR - " twice">];; + " twice">] (*Adds a possible existing interpretation function*) let overwriting_interp_add (ast_typ,interp_fun)= if Hashtbl.mem interp_tab ast_typ then (Hashtbl.remove interp_tab ast_typ; warning ("Overwriting definition of tactic interpreter command "^ast_typ)); - Hashtbl.add interp_tab ast_typ interp_fun;; + Hashtbl.add interp_tab ast_typ interp_fun (*Finds the interpretation function corresponding to a given ast type*) -let look_for_interp=Hashtbl.find interp_tab;; +let look_for_interp=Hashtbl.find interp_tab (*Globalizes the identifier*) let glob_nvar id= try Nametab.sp_of_id CCI id with - Not_found -> error ("unbound variable "^(string_of_id id));; + Not_found -> error ("unbound variable "^(string_of_id id)) (*Summary and Object declaration*) -let mactab=ref Gmap.empty;; +let mactab=ref Gmap.empty -let lookup id=Gmap.find id !mactab;; +let lookup id=Gmap.find id !mactab -let init ()=mactab:=Gmap.empty in -let freeze ()= !mactab in -let unfreeze fs=mactab:=fs in - Summary.declare_summary "tactic-definition" - {Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init};; +let _ = + let init () = mactab := Gmap.empty in + let freeze () = !mactab in + let unfreeze fs = mactab := fs in + Summary.declare_summary "tactic-definition" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } let (inMD,outMD)= let add (na,td)=mactab:=Gmap.add na td !mactab in @@ -101,32 +102,30 @@ let (inMD,outMD)= {cache_function=cache_md; load_function=(fun _ -> ()); open_function=(fun _ -> ()); - specification_function=(fun x -> x)});; + specification_function=(fun x -> x)}) (*Adds a Tactic Definition in the table*) -let add_tacdef na vbody= +let add_tacdef na vbody = if Gmap.mem na !mactab then - errorlabstrm "Tacdef.add_tacdef" [<'sTR - "There is already a Tactic Definition named "; 'sTR na>] - else - let _=Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) - in - mSGNL [<'sTR (na^" is defined")>];; + errorlabstrm "Tacdef.add_tacdef" + [< 'sTR "There is already a Tactic Definition named "; 'sTR na >]; + let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in + if Options.is_verbose() then mSGNL [< 'sTR (na^" is defined") >] (*Unboxes the tactic_arg*) let unvarg=function VArg a -> a - |_ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">];; + |_ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">] (*Unboxes VRec*) let unrec=function VRec v -> !v - |a -> a;; + |a -> a (*Unboxes REDEXP*) let unredexp=function Redexp c -> c - |_ -> errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">];; + |_ -> errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">] (*Reads the head of Fun*) let read_fun ast= @@ -140,7 +139,7 @@ let read_fun ast= match ast with Node(_,"FUNVAR",l) -> read_fun_rec l |_ -> - anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">];; + anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">] (*Reads the clauses of a Rec*) let rec read_rec_clauses=function @@ -149,7 +148,7 @@ let rec read_rec_clauses=function (name,it,body)::(read_rec_clauses tl) |_ -> anomalylabstrm "Tacinterp.read_rec_clauses" [<'sTR - "Rec not well formed">];; + "Rec not well formed">] (*Associates variables with values and gives the remaining variables and values*) @@ -163,24 +162,24 @@ let head_with_value (lvar,lval)= |(vr,[]) -> (lacc,vr,[]) |([],ve) -> (lacc,[],ve) in - head_with_value_rec [] (lvar,lval);; + head_with_value_rec [] (lvar,lval) (*Type of hypotheses for a Match Context rule*) type match_context_hyps= NoHypId of constr_pattern - |Hyp of string*constr_pattern;; + |Hyp of string*constr_pattern (*Type of a Match rule for Match Context and Match*) type match_rule= Pat of match_context_hyps list*constr_pattern*Coqast.t - |All of Coqast.t;; + |All of Coqast.t (*Gives the ast of a COMMAND ast node*) let ast_of_command=function Node(_,"COMMAND",[c]) -> c |ast -> anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",[<'sTR - "Not a COMMAND ast node: ";print_ast ast>]);; + "Not a COMMAND ast node: ";print_ast ast>]) (*Reads the hypotheses of a Match Context rule*) let rec read_match_context_hyps evc env=function @@ -193,7 +192,7 @@ let rec read_match_context_hyps evc env=function |ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",[<'sTR "Not a MATCHCONTEXTHYP ast node: ";print_ast ast>]) - |[] -> [];; + |[] -> [] (*Reads the rules of a Match Context*) let rec read_match_context_rule evc env=function @@ -208,7 +207,7 @@ let rec read_match_context_rule evc env=function |ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR "Not a MATCHCONTEXTRULE ast node: ";print_ast ast>]) - |[] -> [];; + |[] -> [] (*Reads the rules of a Match*) let rec read_match_rule evc env=function @@ -220,18 +219,18 @@ let rec read_match_rule evc env=function |ast::tl -> anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR "Not a MATCHRULE ast node: ";print_ast ast>]) - |[] -> [];; + |[] -> [] (*Transforms a type_judgment signature into a (string*constr) list*) let make_hyps hyps= let lid=List.map string_of_id (ids_of_sign hyps) and lhyp=List.map body_of_type (vals_of_sign hyps) in - List.combine lid lhyp;; + List.combine lid lhyp (*For Match Context and Match*) -exception No_match;; -exception Not_coherent_metas;; +exception No_match +exception Not_coherent_metas (*Verifies if the matched list is coherent with respect to lcm*) let rec verify_metas_coherence lcm=function @@ -245,14 +244,14 @@ let rec verify_metas_coherence lcm=function (num,csr)::(verify_metas_coherence lcm tl) else raise Not_coherent_metas - |[] -> [];; + |[] -> [] (*Tries to match a pattern and a constr*) let apply_matching pat csr= try (Pattern.matches pat csr) with - PatternMatchingFailure -> raise No_match;; + PatternMatchingFailure -> raise No_match (*Tries to match one hypothesis with a list of hypothesis patterns*) let apply_one_hyp_context lmatch mhyps (idhyp,hyp)= @@ -276,7 +275,7 @@ let apply_one_hyp_context lmatch mhyps (idhyp,hyp)= tl) |[] -> raise No_match in - apply_one_hyp_context_rec (idhyp,hyp) [] mhyps;; + apply_one_hyp_context_rec (idhyp,hyp) [] mhyps (*Prepares the lfun list for constr substitutions*) let rec make_subs_list=function @@ -285,7 +284,7 @@ let rec make_subs_list=function |(id,VArg (Constr c))::tl -> (id_of_string id,c)::(make_subs_list tl) |e::tl -> make_subs_list tl - |[] -> [];; + |[] -> [] (*Interprets any expression*) let rec val_interp (evc,env,lfun,lmatch,goalopt) ast= @@ -690,13 +689,13 @@ and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l)=function error "\"Goal\" occurs twice" else (Some (List.map num_of_ast nums), l) - |arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern");; + |arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern") (*Interprets tactic arguments*) -let interp_tacarg sign ast=unvarg (val_interp sign ast);; +let interp_tacarg sign ast=unvarg (val_interp sign ast) (*Initial call for interpretation*) -let interp=tac_interp [] [];; +let interp=tac_interp [] [] let is_just_undef_macro ast = match ast with diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4 index c4d6468dd..d0ef0c5eb 100644 --- a/scripts/coqc.ml4 +++ b/scripts/coqc.ml4 @@ -18,6 +18,7 @@ let environment = Unix.environment () let bindir = ref Coq_config.bindir +let binary = ref "coqtop.byte" (* the $COQBIN environment variable has priority over the Coq_config value *) let _ = @@ -114,6 +115,8 @@ let parse_args () = bindir := d ; parse (cfiles,args) rem | "-bindir" :: [] -> usage () + | "-opt" :: rem -> + binary := "coqtop.opt"; parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-image"|"-libdir"|"-I"|"-R"|"-include"|"-outputstate"|"-inputstate" |"-is"|"-load-vernac-source"|"-load-vernac-object"|"-load-ml-source" @@ -125,7 +128,7 @@ let parse_args () = | [] -> usage () end | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" - |"-q"|"-opt"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem -> + |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" as o) :: rem -> parse (cfiles,o::args) rem | f :: rem -> if Sys.file_exists f then @@ -150,7 +153,7 @@ let main () = prerr_endline "coqc: too few arguments" ; usage () end; - let coqtopname = Filename.concat !bindir "coqtop.byte" in + let coqtopname = Filename.concat !bindir !binary in List.iter (compile coqtopname args) cfiles let _ = Printexc.print main (); exit 0 diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index a148c7695..e087271ae 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -49,15 +49,11 @@ let notopobjs = gramobjs (* 5. High-level tactics objects *) let hightactics = split_cmo Tolink.hightactics -let cmotacsobjs = [ - "prolog.cmo"; "equality.cmo"; "inv.cmo"; "leminv.cmo"; - "point.cmo"; "progmach.cmo"; "program.cmo"; "propre.cmo"; - "tauto.cmo"; "gelim.cmo"; "eqdecide.cmo"] (* environment *) let src_coqtop = ref Coq_config.coqtop -let notactics = ref false let opt = ref false +let full = ref false let top = ref false let searchisos = ref false let echo = ref false @@ -98,10 +94,9 @@ let module_of_file name = let files_to_link userfiles = let dyn_objs = if not !opt then dynobjs else [] in let command_objs = if !searchisos then coqsearch else [] in - let tactic_objs = if !notactics then [] else hightactics in let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in - let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ tactic_objs @ + let objs = core_objs @ dyn_objs @ toplevel @ command_objs @ hightactics @ toplevel_objs in let tolink = if !opt then @@ -142,11 +137,11 @@ let usage () = prerr_endline "Usage: coqmktop <options> <ocaml options> files Options are: -srcdir dir Specify where the Coq source files are - -notactics Do not link high level tactics -o exec-file Specify the name of the resulting toplevel -opt Compile in native code + -full Link high level tactics -top Build Coq on a ocaml toplevel (incompatible with -opt) - -searchisos Build a toplevel for SearchIsos (implies -notactics) + -searchisos Build a toplevel for SearchIsos -R dir Specify recursively directories for Ocaml\n"; exit 1 @@ -156,11 +151,11 @@ let parse_args () = | [] -> List.rev op, List.rev fl | "-srcdir" :: d :: rem -> src_coqtop := d ; parse (op,fl) rem | "-srcdir" :: _ -> usage () - | "-notactics" :: rem -> notactics := true ; parse (op,fl) rem | "-opt" :: rem -> opt := true ; parse (op,fl) rem + | "-full" :: rem -> full := true ; parse (op,fl) rem | "-top" :: rem -> top := true ; parse (op,fl) rem | "-searchisos" :: rem -> - searchisos := true; notactics := true; parse (op,fl) rem + searchisos := true; parse (op,fl) rem | "-echo" :: rem -> echo := true ; parse (op,fl) rem | ("-cclib"|"-ccopt"|"-I"|"-o" as o) :: rem' -> begin |