aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.make8
-rw-r--r--checker/checker.ml14
-rw-r--r--config/coq_config.mli2
-rw-r--r--configure.ml27
-rw-r--r--doc/changelog/10-standard-library/13080-ascii.rst4
-rw-r--r--ide/coqide/coq.ml21
-rw-r--r--ide/coqide/idetop.ml4
-rw-r--r--sysinit/usage.ml5
-rw-r--r--theories/Strings/Ascii.v8
-rw-r--r--tools/coqdoc/main.ml3
-rw-r--r--toplevel/coqtop.ml10
11 files changed, 38 insertions, 68 deletions
diff --git a/Makefile.make b/Makefile.make
index 2f6781439c..eeb3e9b539 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -274,7 +274,7 @@ depclean:
find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} +
cacheclean:
- find theories test-suite -name '.*.aux' -exec rm -f {} +
+ find theories user-contrib test-suite -name '.*.aux' -exec rm -f {} +
cleanconfig:
rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist
@@ -282,12 +282,12 @@ cleanconfig:
distclean: clean cleanconfig cacheclean timingclean
voclean:
- find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \
+ find theories plugins user-contrib test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \
-o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} +
- find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} +
+ find theories plugins user-contrib test-suite -name .coq-native -empty -exec rm -rf {} +
timingclean:
- find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \
+ find theories plugins user-contrib test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \
-o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \
-o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \
-o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} +
diff --git a/checker/checker.ml b/checker/checker.ml
index 588ce14336..ba5e3c6d1a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -48,19 +48,17 @@ let path_of_string s =
let ( / ) = Filename.concat
-let get_version_date () =
+let get_version () =
try
let ch = open_in (Envars.coqlib () / "revision") in
let ver = input_line ch in
let rev = input_line ch in
let () = close_in ch in
- (ver,rev)
- with _ -> (Coq_config.version,Coq_config.date)
+ Printf.sprintf "%s (%s)" ver rev
+ with _ -> Coq_config.version
let print_header () =
- let (ver,rev) = (get_version_date ()) in
- Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
- flush stdout
+ Printf.printf "Welcome to Chicken %s\n%!" (get_version ())
(* Adding files to Coq loadpath *)
@@ -168,9 +166,7 @@ let compile_files senv =
~check:(List.rev !compile_list)
let version () =
- Printf.printf "The Coq Proof Checker, version %s (%s)\n"
- Coq_config.version Coq_config.date;
- Printf.printf "compiled on %s\n" Coq_config.compile_date;
+ Printf.printf "The Coq Proof Checker, version %s\n" Coq_config.version;
exit 0
(* print the usage of coqtop (or coqc) on channel co *)
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 809fa3d758..035574475d 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -33,8 +33,6 @@ val arch_is_win32 : bool
val version : string (* version number of Coq *)
val caml_version : string (* OCaml version used to compile Coq *)
val caml_version_nums : int list (* OCaml version used to compile Coq by components *)
-val date : string (* release date *)
-val compile_date : string (* compile date *)
val vo_version : int32
val state_magic_number : int
diff --git a/configure.ml b/configure.ml
index 40d77ed109..7814204e42 100644
--- a/configure.ml
+++ b/configure.ml
@@ -196,31 +196,6 @@ let which prog =
let program_in_path prog =
try let _ = which prog in true with Not_found -> false
-let build_date =
- try
- float_of_string (Sys.getenv "SOURCE_DATE_EPOCH")
- with
- Not_found -> Unix.time ()
-
-(** * Date *)
-
-(** The short one is displayed when starting coqtop,
- The long one is used as compile date *)
-
-let months =
- [| "January";"February";"March";"April";"May";"June";
- "July";"August";"September";"October";"November";"December" |]
-
-let get_date () =
- let now = Unix.gmtime build_date in
- let year = 1900+now.Unix.tm_year in
- let month = months.(now.Unix.tm_mon) in
- sprintf "%s %d" month year,
- sprintf "%s %d %d %d:%02d:%02d" (String.sub month 0 3) now.Unix.tm_mday year
- now.Unix.tm_hour now.Unix.tm_min now.Unix.tm_sec
-
-let short_date, full_date = get_date ()
-
(** * Command-line parsing *)
type ide = Opt | Byte | No
@@ -1096,8 +1071,6 @@ let write_configml f =
pr_s "version" coq_version;
pr_s "caml_version" caml_version;
pr_li "caml_version_nums" caml_version_nums;
- pr_s "date" short_date;
- pr_s "compile_date" full_date;
pr_s "arch" arch;
pr_b "arch_is_win32" arch_is_win32;
pr_s "exec_extension" exe;
diff --git a/doc/changelog/10-standard-library/13080-ascii.rst b/doc/changelog/10-standard-library/13080-ascii.rst
new file mode 100644
index 0000000000..167002283e
--- /dev/null
+++ b/doc/changelog/10-standard-library/13080-ascii.rst
@@ -0,0 +1,4 @@
+- **Added:**
+ ``leb`` and ``ltb`` functions for ``ascii``
+ (`#13080 <https://github.com/coq/coq/pull/13080>`_,
+ by Yishuai Li).
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml
index b8228df2aa..20e9f0134f 100644
--- a/ide/coqide/coq.ml
+++ b/ide/coqide/coq.ml
@@ -13,13 +13,9 @@ open Preferences
let ideslave_coqtop_flags = ref None
-(** * Version and date *)
+(** * Version *)
-let get_version_date () =
- let date =
- if Glib.Utf8.validate Coq_config.date
- then Coq_config.date
- else "<date not printable>" in
+let get_version () =
try
(* the following makes sense only when running with local layout *)
let coqroot = Filename.concat
@@ -29,21 +25,20 @@ let get_version_date () =
let ch = open_in (Filename.concat coqroot "revision") in
let ver = input_line ch in
let rev = input_line ch in
- (ver,rev)
- with _ -> (Coq_config.version,date)
+ close_in ch;
+ Printf.sprintf "%s (%s)" ver rev
+ with _ -> Coq_config.version
let short_version () =
- let (ver,date) = get_version_date () in
- Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date
+ Printf.sprintf "The Coq Proof Assistant, version %s\n" (get_version ())
let version () =
- let (ver,date) = get_version_date () in
Printf.sprintf
- "The Coq Proof Assistant, version %s (%s)\
+ "The Coq Proof Assistant, version %s\
\nArchitecture %s running %s operating system\
\nGtk version is %s\
\nThis is %s \n"
- ver date
+ (get_version ())
Coq_config.arch Sys.os_type
(let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
(Filename.basename Sys.executable_name)
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 4b069b09ba..a6a7f7d742 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -397,8 +397,8 @@ let set_options options =
let about () = {
Interface.coqtop_version = Coq_config.version;
Interface.protocol_version = Xmlprotocol.protocol_version;
- Interface.release_date = Coq_config.date;
- Interface.compile_date = Coq_config.compile_date;
+ Interface.release_date = "n/a";
+ Interface.compile_date = "n/a";
}
let handle_exn (e, info) =
diff --git a/sysinit/usage.ml b/sysinit/usage.ml
index 763cd54137..d00b916f23 100644
--- a/sysinit/usage.ml
+++ b/sysinit/usage.ml
@@ -9,9 +9,8 @@
(************************************************************************)
let version () =
- Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
- Coq_config.version Coq_config.date;
- Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version
+ Printf.printf "The Coq Proof Assistant, version %s\n" Coq_config.version;
+ Printf.printf "compiled with OCaml %s\n" Coq_config.caml_version
let machine_readable_version () =
Printf.printf "%s %s\n"
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 06b02ab211..37d30a282c 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -173,6 +173,14 @@ Proof.
apply N_ascii_bounded.
Qed.
+Definition ltb (a b : ascii) : bool :=
+ (N_of_ascii a <? N_of_ascii b)%N.
+
+Definition leb (a b : ascii) : bool :=
+ (N_of_ascii a <=? N_of_ascii b)%N.
+
+Infix "<?" := ltb : char_scope.
+Infix "<=?" := leb : char_scope.
(** * Concrete syntax *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 6ebf9b71d6..b8d5032373 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -87,8 +87,7 @@ let obsolete s =
course). *)
let banner () =
- eprintf "This is coqdoc version %s, compiled on %s\n"
- Coq_config.version Coq_config.compile_date;
+ eprintf "This is coqdoc version %s\n" Coq_config.version;
flush stderr
let target_full_name f =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 32e942f0d0..bb44d9cdee 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -18,19 +18,17 @@ let () = at_exit flush_all
let ( / ) = Filename.concat
-let get_version_date () =
+let get_version () =
try
let ch = open_in (Envars.coqlib () / "revision") in
let ver = input_line ch in
let rev = input_line ch in
let () = close_in ch in
- (ver,rev)
- with e when CErrors.noncritical e ->
- (Coq_config.version,Coq_config.date)
+ Printf.sprintf "%s (%s)" ver rev
+ with _ -> Coq_config.version
let print_header () =
- let (ver,rev) = get_version_date () in
- Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
+ Feedback.msg_info (str "Welcome to Coq " ++ str (get_version ()));
flush_all ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 03:12:57 +0000