else
OCAMLFIND = @OCAMLFIND@
endif
-CAMLP4O = @CAMLP4O@
+CAMLP5O = @CAMLP5O@
LABLGLADECC = @LABLGLADECC@
HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
DISTRIBUTED = @DISTRIBUTED@
-requires="helm-acic_content helm-syntax_extensions camlp4.gramlib ulex helm-grafite"
+requires="helm-acic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite"
version="0.0.1"
archive(byte)="content_pres.cma"
archive(native)="content_pres.cmxa"
-requires="unix camlp4.gramlib"
+requires="unix camlp5.gramlib"
version="0.0.1"
archive(byte)="extlib.cma"
archive(native)="extlib.cmxa"
-requires="helm-lexicon helm-grafite ulex"
+requires="helm-lexicon helm-grafite ulex08"
version="0.0.1"
archive(byte)="grafite_parser.cma"
archive(native)="grafite_parser.cmxa"
-requires="helm-content_pres helm-cic_disambiguation camlp4.gramlib"
+requires="helm-content_pres helm-cic_disambiguation camlp5.gramlib"
version="0.0.1"
archive(byte)="lexicon.cma"
archive(native)="lexicon.cmxa"
version="0.0.1"
archive(byte)="utf8_macros.cma"
archive(native)="utf8_macros.cmxa"
-requires(syntax,preprocessor)="camlp4"
+requires(syntax,preprocessor)="camlp5"
archive(syntax,preprocessor)="pa_extend.cmo pa_unicode_macro.cma profiling_macros.cma"
linkopts=""
# $OCAMLFIND must be set to a meaningful vaule, including OCAMLPATH=
-PREPROCOPTIONS = -pp camlp4o
-SYNTAXOPTIONS = -syntax camlp4o
+PREPROCOPTIONS = -pp camlp5o
+SYNTAXOPTIONS = -syntax camlp5o
PREREQ =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes
OCAMLDEBUGOPTIONS = -g
#OCAML_PROF=p -p a
OCAMLARCHIVEOPTIONS =
OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS)
#OCAMLOPT_DEBUG_FLAGS = -p
OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS) $(OCAMLOPT_DEBUG_FLAGS)
-OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp4 $(CAMLP4REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS)
+OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp5 $(CAMLP5REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS)
OCAMLLEX = ocamllex
OCAMLYACC = ocamlyacc
type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
type fold_kind = [ `Left | `Right ]
-type location = Token.flocation
+type location = Stdpp.location
let fail floc msg =
let (x, y) = HExtlib.loc_of_floc floc in
failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
extractor: extractor.ml
$(H)echo " OCAMLC $<"
$(H)$(OCAMLFIND) ocamlc \
- -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $<
extractor.opt: extractor.ml
$(H)echo " OCAMLOPT $<"
$(H)$(OCAMLFIND) ocamlopt \
- -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $<
extractor_manager: extractor_manager.ml
$(H)echo " OCAMLC $<"
$(H)$(OCAMLFIND) ocamlc \
- -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $<
extractor_manager.opt: extractor_manager.ml
$(H)echo " OCAMLOPT $<"
$(H)$(OCAMLFIND) ocamlopt \
- -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $<
export: extractor.opt extractor_manager.opt
nice -n 20 \
CMIS = $(MLIS:%.mli=%.cmi)
EXTRAS =
-OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg
-OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg
+OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -rectypes
+OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg -rectypes
OCAMLDEP = $(OCAMLFIND) ocamldep
OCAMLYACC = ocamlyacc
OCAMLLEX = ocamllex
table_creator: table_creator.ml
$(H)echo " OCAMLC $<"
$(H)$(OCAMLFIND) ocamlc \
- -thread -package mysql,helm-metadata -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata -linkpkg -rectypes -o $@ $<
table_destructor: table_creator
$(H)ln -f $< $@
table_creator.opt: table_creator.ml
$(H)echo " OCAMLOPT $<"
$(H)$(OCAMLFIND) ocamlopt \
- -thread -package mysql,helm-metadata -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata -linkpkg -rectypes -o $@ $<
table_destructor.opt: table_creator.opt
$(H)ln -f $< $@
CMIS = $(MLIS:%.mli=%.cmi)
EXTRAS =
-OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg
-OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg
+OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -rectypes
+OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg -rectypes
OCAMLDEP = $(OCAMLFIND) ocamldep
OCAMLYACC = ocamlyacc
OCAMLLEX = ocamllex
UTILITIES = create_environment parse_library list_uris test_library
UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES))
-LINKOPTS = -linkpkg -thread
+LINKOPTS = -linkpkg -rectypes -thread
LIBS = helm-cic_proof_checking
OCAMLC = $(OCAMLFIND) ocamlc $(LINKOPTS) -package $(LIBS)
OCAMLOPT = $(OCAMLFIND) opt $(LINKOPTS) -package $(LIBS)
(* the integer is an offset to be added to each location *)
exception NoWellTypedInterpretation of
int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Token.flocation option * string Lazy.t * bool) list
+ Stdpp.location option * string Lazy.t * bool) list
exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
type 'a disambiguator_input = string * int * 'a
type domain = domain_tree list
-and domain_tree = Node of Token.flocation list * domain_item * domain
+and domain_tree = Node of Stdpp.location list * domain_item * domain
let rec string_of_domain =
function
type 'a test_result =
| Ok of 'a * Cic.metasenv
- | Ko of Token.flocation option * string Lazy.t
- | Uncertain of Token.flocation option * string Lazy.t
+ | Ko of Stdpp.location option * string Lazy.t
+ | Uncertain of Stdpp.location option * string Lazy.t
let refine_term metasenv context uri term ugraph ~localization_tbl =
(* if benchmark then incr actual_refinements; *)
* useless for the final user ... *)
exception NoWellTypedInterpretation of
int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Token.flocation option * string Lazy.t * bool) list
+ Stdpp.location option * string Lazy.t * bool) list
exception PathNotWellFormed
val interpretate_path :
UriManager.uri list
val interactive_interpretation_choice:
string -> int ->
- (Token.flocation list * string * string) list list -> int list
+ (Stdpp.location list * string * string) list list -> int list
val input_or_locate_uri:
title:string -> ?id:string -> unit -> UriManager.uri option
end
val interactive_interpretation_choice :
string -> int ->
- (Token.flocation list * string * string) list list -> int list
+ (Stdpp.location list * string * string) list list -> int list
(** @param title gtk window title for user prompting
* @param id unbound identifier which originated this callback invocation *)
include ../../Makefile.defs
include ../Makefile.common
-
-cicReduction.cmo: OCAMLOPTIONS+=-rectypes
-cicReduction.cmx: OCAMLOPTIONS+=-rectypes
-
(* refines [term] and returns the refined form of [term], *)
(* its type, the new metasenv and universe graph. *)
val type_of_aux':
- ?localization_tbl:Token.flocation Cic.CicHash.t ->
+ ?localization_tbl:Stdpp.location Cic.CicHash.t ->
Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph
(* the new metasenv and universe graph. *)
(* the [uri] is required only for inductive definitions *)
val typecheck :
- localization_tbl:Token.flocation Cic.CicHash.t ->
+ localization_tbl:Stdpp.location Cic.CicHash.t ->
Cic.metasenv -> UriManager.uri option -> Cic.obj ->
Cic.obj * Cic.metasenv * CicUniv.universe_graph
# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by
# "_loc" occurrences
UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions)
-ULEXDIR := $(shell $(OCAMLFIND) query ulex)
-MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
+ULEXDIR := $(shell $(OCAMLFIND) query ulex08)
+MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
cicNotationParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
cicNotationLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
raise (Error (begin_cnum, end_cnum, msg))
let return_with_loc token begin_cnum end_cnum =
- (* TODO handle line/column numbers *)
- let flocation_begin =
- { Lexing.pos_fname = "";
- Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
- Lexing.pos_cnum = begin_cnum }
- in
- let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in
- (token, (flocation_begin, flocation_end))
+ let flocation = HExtlib.floc_of_loc (begin_cnum,end_cnum) in
+ token, flocation
let return lexbuf token =
let begin_cnum, end_cnum = Ulexing.loc lexbuf in
(* let lexbuf = Ulexing.from_utf8_stream stream in *)
(** XXX Obj.magic rationale.
* The problem.
- * camlp4 constraints the tok_func field of Token.glexer to have type:
+ * camlp5 constraints the tok_func field of Token.glexer to have type:
* Stream.t char -> (Stream.t 'te * flocation_function)
* In order to use ulex we have (in theory) to instantiate a new lexbuf each
* time a char Stream.t is passed, destroying the previous lexbuf which may
* have consumed a character from the old stream which is lost forever :-(
* The "solution".
- * Instead of passing to camlp4 a char Stream.t we pass a lexbuf, casting it to
+ * Instead of passing to camlp5 a char Stream.t we pass a lexbuf, casting it to
* char Stream.t with Obj.magic where needed.
*)
let lexbuf = Obj.magic stream in
- Token.make_stream_and_flocation
+ Token.make_stream_and_location
(fun () ->
try
token lexbuf
in
string_of_int precedence ^ assoc_string
-type rule_id = Token.t Gramext.g_symbol list
+type rule_id = Grammar.token Gramext.g_symbol list
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
let owned_keywords = Hashtbl.create 23
(** {2 Localized exceptions } *)
-exception Localized of Token.flocation * exn
+exception Localized of Stdpp.location * exn
-let loc_of_floc = function
- | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
- (loc_begin, loc_end)
+let loc_of_floc floc = Stdpp.first_pos floc, Stdpp.last_pos floc;;
let floc_of_loc (loc_begin, loc_end) =
- let floc_begin =
- { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
- Lexing.pos_cnum = loc_begin }
- in
- let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
- (floc_begin, floc_end)
+ Stdpp.make_loc (loc_begin, loc_end)
let dummy_floc = floc_of_loc (-1, -1)
let raise_localized_exception ~offset floc exn =
- let (x, y) = loc_of_floc floc in
+ let x, y = loc_of_floc floc in
let x = offset + x in
let y = offset + y in
- let flocb,floce = floc in
- let floc =
- { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y }
- in
+ let floc = floc_of_loc (x,y) in
raise (Localized (floc, exn))
let estimate_size x =
(** {2 Localized exceptions } *)
-exception Localized of Token.flocation * exn
+exception Localized of Stdpp.location * exn
-val loc_of_floc: Token.flocation -> int * int
-val floc_of_loc: int * int -> Token.flocation
+val loc_of_floc: Stdpp.location -> int * int
+val floc_of_loc: int * int -> Stdpp.location
-val dummy_floc: Lexing.position * Lexing.position
+val dummy_floc: Stdpp.location
-val raise_localized_exception: offset:int -> Token.flocation -> exn -> 'a
+val raise_localized_exception: offset:int -> Stdpp.location -> exn -> 'a
(* size in KB (SLOW) *)
val estimate_size: 'a -> int
type direction = [ `LeftToRight | `RightToLeft ]
-type loc = Token.flocation
+type loc = Stdpp.location
type ('term, 'lazy_term, 'ident) pattern =
'lazy_term option * ('ident * 'term) list * 'term option
# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by
# "_loc" occurrences
UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions)
-ULEXDIR = $(shell $(OCAMLFIND) query ulex)
-MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
+ULEXDIR = $(shell $(OCAMLFIND) query ulex08)
+MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
(* the integer is an offset to be added to each location *)
exception DisambiguationError of
int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Token.flocation option * string Lazy.t * bool) list list
+ Stdpp.location option * string Lazy.t * bool) list list
(** parameters are: option name, error message *)
exception Unbound_identifier of string
type choose_interp_callback =
string -> int ->
- (Token.flocation list * string * string) list list -> int list
+ (Stdpp.location list * string * string) list list -> int list
let mono_uris_callback ~id =
if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
(* the integer is an offset to be added to each location *)
exception DisambiguationError of
int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Token.flocation option * string Lazy.t * bool) list list
+ Stdpp.location option * string Lazy.t * bool) list list
(** parameters are: option name, error message *)
(** initially false; for debugging only (???) *)
type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
type choose_interp_callback =
- string -> int -> (Token.flocation list * string * string) list list ->
+ string -> int -> (Stdpp.location list * string * string) list list ->
int list
val set_choose_uris_callback: choose_uris_callback -> unit
type direction = [ `LeftToRight | `RightToLeft ]
-type loc = Token.flocation
+type loc = Stdpp.location
type alias_spec =
| Ident_alias of string * string (* identifier, uri *)
(* these are the same functions of cic_unification/ (eventually wrapped) *)
type kit = {
type_of_aux':
- ?localization_tbl:Token.flocation Cic.CicHash.t ->
+ ?localization_tbl:Stdpp.location Cic.CicHash.t ->
Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
type_of_rc;
pack_coercion_obj: Cic.obj -> Cic.obj;
./make_table $@
utf8MacroTable.cmo: utf8MacroTable.ml
@echo " OCAMLC $<"
- $(H)@$(OCAMLFIND) ocamlc -c $<
+ $(H)@$(OCAMLFIND) ocamlc -c -rectypes $<
pa_unicode_macro.cmo: pa_unicode_macro.ml utf8Macro.cmo
@echo " OCAMLC $<"
- $(H)@$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o q_MLast.cmo pa_extend.cmo -loc loc" -c $<
+ $(H)@$(OCAMLFIND) ocamlc -package camlp5 -rectypes -pp "camlp5o q_MLast.cmo pa_extend.cmo -loc loc" -c $<
pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo
@echo " OCAMLC -a $@"
$(H)@$(OCAMLFIND) ocamlc -a -o $@ $^
profiling_macros.cmo: profiling_macros.ml
@echo " OCAMLC $<"
- $(H)@$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o -loc loc" -c $<
+ $(H)@$(OCAMLFIND) ocamlc -package camlp5 -pp "camlp5o -loc loc" -c $<
profiling_macros.cma:profiling_macros.cmo
@echo " OCAMLC -a $@"
$(H)@$(OCAMLFIND) ocamlc -a -o $@ $^
.PHONY: test
test: test.ml
- $(OCAMLFIND) ocamlc -package helm-utf8_macros -syntax camlp4o $< -o $@
+ $(OCAMLFIND) ocamlc -package helm-utf8_macros -syntax camlp5o $< -o $@
clean:
distclean: extra_clean
Compile it with:
- ocamlfind ocamlc -package helm-utf8_macros -syntax camlp4o test.ml
+ ocamlfind ocamlc -package helm-utf8_macros -syntax camlp5o test.ml
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s)
-let loc =
- let dummy_pos =
- { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
- Lexing.pos_cnum = -1 }
- in
- (dummy_pos, dummy_pos)
+let loc = Stdpp.make_loc (-1, -1)
let expand_unicode_macro macro =
debug_print (lazy (Printf.sprintf "Expanding macro '%s' ..." macro));
UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions)
STR=$(shell $(OCAMLFIND) query str)
-MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(STR) str.cma pa_extend.cmo profiling_macros.cma -loc loc"
+MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(STR) str.cma pa_extend.cmo profiling_macros.cma -loc loc"
paramodulation/%.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
paramodulation/%.cmo: OCAMLC = $(OCAMLC_P4)
paramodulation/%.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
else
AC_MSG_ERROR(could not find lablgladecc2)
fi
-AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no)
-if test $HAVE_CAMLP4O = "yes"; then
- CAMLP4O="camlp4o"
+AC_CHECK_PROG(HAVE_CAMLP5O, camlp5o, yes, no)
+if test $HAVE_CAMLP5O = "yes"; then
+ CAMLP5O="camlp5o"
else
- AC_MSG_ERROR(could not find camlp4o)
+ AC_MSG_ERROR(could not find camlp5o)
fi
# look for METAS dir
fi
AC_MSG_RESULT($MSG)
-AC_SUBST(CAMLP4O)
+AC_SUBST(CAMLP5O)
AC_SUBST(DBHOST)
AC_SUBST(DEBUG)
AC_SUBST(DISTRIBUTED)
NULL =
H=@
-OCAML_FLAGS = -pp $(CAMLP4O)
+OCAML_FLAGS = -pp $(CAMLP5O) -rectypes
PKGS = -package "$(MATITA_REQUIRES)"
CPKGS = -package "$(MATITA_CREQUIRES)"
OCAML_THREADS_FLAGS = -thread
apply (not_le_Sn_n ? H3).
qed.
-theorem lt_S_S: ∀n,m. n < m → S n < S m.
-intros;
-unfold lt in H;
-apply (le_S_S ? ? H).
-qed.
+
(* moved to nat/order.ma
theorem lt_O_S: ∀n. O < S n.
intros. apply le_S_S_to_le. assumption.
qed.
+theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
+intros;
+unfold lt in H;
+apply (le_S_S ? ? H).
+qed.
+
theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
intros.elim H.exact I.exact I.
qed.
let (x, y) = HExtlib.loc_of_floc floc in
let x = x + offset in
let y = y + offset in
- let flocb,floce = floc in
- let floc =
- {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y}
- in
+ let floc = HExtlib.floc_of_loc (x,y) in
Some floc
| _ -> None in
let rec explain =
* http://helm.cs.unibo.it/
*)
-val to_string: exn -> Token.flocation option * string
+val to_string: exn -> Stdpp.location option * string
(* given an utf8 string a floc returns the parsed substring and its length
* in bytes *)
-val utf8_parsed_text: string -> Token.flocation -> string * int
+val utf8_parsed_text: string -> Stdpp.location -> string * int
(* the length in characters, not bytes *)
val utf8_string_length: string -> int
projects / helm.git / commitdiff