aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile12
-rwxr-xr-xconfigure50
-rw-r--r--ide/.coqide-gtk2rc6
-rw-r--r--ide/FAQ8
-rw-r--r--ide/preferences.ml4
-rw-r--r--ide/utf8.v54
6 files changed, 84 insertions, 50 deletions
diff --git a/Makefile b/Makefile
index 58cf559ce..97d8141cf 100644
--- a/Makefile
+++ b/Makefile
@@ -409,12 +409,12 @@ beforedepend:: ide/utf8_convert.ml
FULLIDELIB=$(FULLCOQLIB)/ide
-OLDCOQIDEVO=ide/utf8.vo
+COQIDEVO=ide/utf8.vo
-$(OLDCOQIDEVO): states/initial.coq states7/initial.coq
- $(BOOTCOQTOP) $(TRANSLATE) -compile $*
+$(COQIDEVO): states/initial.coq
+ $(BOOTCOQTOP) -compile $*
-IDEFILES=$(OLDCOQIDEVO) ide/coq.png ide/.coqide-gtk2rc ide/FAQ
+IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.png ide/.coqide-gtk2rc
coqide: $(IDEFILES) coqide-$(HASCOQIDE)
coqide-no:
@@ -424,7 +424,7 @@ coqide-opt: $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
ide: coqide-$(HASCOQIDE) states
clean-ide:
- rm -f $(OLDCOQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT)
+ rm -f $(COQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT)
$(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) ide.cmxa
$(SHOW)'COQMKTOP -o $@'
@@ -466,7 +466,7 @@ clean::
rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml
rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
rm -f ide/utf8_convert.ml
- rm -f $(OLDCOQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi)
+ rm -f $(COQIDEVO) $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi)
rm -f $(COQIDEBYTE) $(COQIDEOPT)
# coqc
diff --git a/configure b/configure
index a0c0a4d23..74cfbb05d 100755
--- a/configure
+++ b/configure
@@ -302,32 +302,39 @@ fi
# For coqmktop
-CAMLLIB=`"$CAMLC" -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' `
+#CAMLLIB=`"$CAMLC" -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' `
+CAMLLIB=`"$CAMLC" -where`
# Camlp4 (greatly simplified since merged with ocaml)
CAMLP4BIN=${CAMLBIN}
-case $OS in
- Win32)
- CAMLP4LIB=+camlp4;;
- *)
- CAMLP4LIB=${CAMLLIB}/camlp4
-esac
+#case $OS in
+# Win32)
+ CAMLP4LIB=+camlp4
+# ;;
+# *)
+# CAMLP4LIB=${CAMLLIB}/camlp4
+#esac
# lablgtk2 and CoqIDE
if [ "$coqide_spec" = "no" ] ; then
-if test -x ${CAMLLIB}/lablgtk2; then
- if grep -q -w convert_with_fallback ${CAMLLIB}/lablgtk2/glib.mli; then
- COQIDE=byte
- # native threads
- if test -f ${CAMLLIB}/threads/threads.cmxa; then
+if test -x "${CAMLLIB}/lablgtk2" ; then
+ if grep -q -w convert_with_fallback "${CAMLLIB}/lablgtk2/glib.mli" ; then
+ if test -f "${CAMLLIB}/threads/threads.cmxa" ; then
+ echo "LablGtk2 found, native threads: native CoqIde will be available"
COQIDE=opt;
+ else
+ echo "LablGtk2 found, no native threads: bytecode CoqIde will be available"
+ COQIDE=byte
fi;
- else COQIDE=no;
+ else
+ echo "LablGtk2 found but too old: CoqIde will not be available"
+ COQIDE=no;
fi
else
+ echo "LablGtk2 not found: CoqIde will not be available"
COQIDE=no
fi
fi
@@ -340,7 +347,8 @@ rm config/giveostype
case $ARCH in
win32)
- STRIPCOMMAND="true";;
+ # true -> strip : it exists under cygwin !
+ STRIPCOMMAND="strip";;
*)
if [ "$coq_profile_flag" = "-p" ] ; then
STRIPCOMMAND="true"
@@ -381,12 +389,12 @@ echo ""
rm -f $COQTOP/config/Makefile
-case $ARCH in
- win32)
- BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'`
- LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'`
- MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'`;;
-esac
+#case $ARCH in
+# win32)
+# BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'`
+# LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'`
+# MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'`;;
+#esac
sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|COQTOPDIRECTORY|$COQTOP|" \
@@ -462,7 +470,7 @@ PRINTF=`which printf`
# Subdirectories of theories/ added in coq_config.ml
subdirs () {
- (cd $1; find * -type d ! -name CVS -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test >> $mlconfig_file)
+ (cd $1; find * -type d ! -name CVS -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> $mlconfig_file)
}
echo "let theories_dirs = [" >> $mlconfig_file
diff --git a/ide/.coqide-gtk2rc b/ide/.coqide-gtk2rc
index 7a74a469d..11c53dad2 100644
--- a/ide/.coqide-gtk2rc
+++ b/ide/.coqide-gtk2rc
@@ -17,8 +17,8 @@ binding "text" {
bind "<ctrl>w" { "cut-clipboard" () }
# For UTF-8 inputs !
- bind "F11" {"insert-at-cursor" ("∀")}
- bind "F12" {"insert-at-cursor" ("∃")}
+# bind "F11" {"insert-at-cursor" ("∀")}
+# bind "F12" {"insert-at-cursor" ("∃")}
}
class "GtkTextView" binding "text"
@@ -36,7 +36,7 @@ widget "*.*.*.*.MessageWindow" style "views"
gtk-font-name = "Sans 12"
style "location" {
-font_name = "Monospace 10"
+font_name = "Sans 10"
}
widget "*location*" style "location"
diff --git a/ide/FAQ b/ide/FAQ
index e20d113a5..2079ef6ce 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -17,8 +17,8 @@ Q4) How to use those Forall and Exists pretty symbols?
R4) Thanks to the Notation features in Coq, you just need to insert these
lines in your Coq Buffer :
======================================================================
-Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10).
-Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
+Notation "∀ x : t, P" := (forall x:t, P) (at level 200, x ident).
+Notation "∃ x : t, P" := (exists x:t, P) (at level 200, x ident).
======================================================================
Copy/Paste of these lines from this file will not work outside of CoqIde.
You need to load a file containing these lines or to enter the "∀"
@@ -58,9 +58,9 @@ R6) Use
Q7) How to customize the shortcuts for menus?
R7) Two solutions are offered:
- Edit $HOME/.coqide.keys by hand or
- - Add "gtk-can-change-accels = 1" in your .coqiderc.gtk2 file. Then
+ - Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
from CoqIde, you may select a menu entry and press the desired
- shortcut. Do not forget to save your preferences.
+ shortcut.
Q8) What encoding should I use? What is this \x{iiii} in my file?
R8) The encoding option is related to the way files are saved.
diff --git a/ide/preferences.ml b/ide/preferences.ml
index ad0c19743..309cc150e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -130,7 +130,7 @@ let (current:pref ref) =
cmd_browse = "netscape -remote \"OpenURL(", ")\"";
cmd_editor = "emacs ", "";
- text_font = Pango.Font.from_string "Monospace 12";
+ text_font = Pango.Font.from_string "sans 12";
doc_url = "http://coq.inria.fr/doc/";
library_url = "http://coq.inria.fr/library/";
@@ -294,7 +294,7 @@ let configure () =
let box = GPack.hbox () in
let w = GMisc.font_selection () in
w#set_preview_text
- "Lemma Truth: ∀ p:Prover, `p < Coq`. Proof. Auto with *. Save.";
+ "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
box#pack w#coerce;
ignore (w#misc#connect#realize
~callback:(fun () -> w#set_font_name
diff --git a/ide/utf8.v b/ide/utf8.v
index 98c2e9638..8428d2e3c 100644
--- a/ide/utf8.v
+++ b/ide/utf8.v
@@ -1,23 +1,49 @@
(* Logic *)
-Notation "∀ x : t , P" := (x:t)P (at level 1, x,t,P at level 10).
-Notation "∀ x y : t , P" := (x:t)(y:t)P (at level 1, x,y,t,P at level 10).
-Notation "∀ x y z : t , P" := (x:t)(y:t)(z:t) P (at level 1, x,y,z,t,P at level 10).
-Notation "∀ x y z u : t , P" := (x:t)(y:t)(z:t)(u:t)P (at level 1, x,y,z,u,t,P at level 10).
+Notation "∀ x , P" :=
+ (forall x , P) (at level 200, x ident) : type_scope.
+Notation "∀ x y , P" :=
+ (forall x y , P) (at level 200, x ident, y ident) : type_scope.
+Notation "∀ x y z , P" :=
+ (forall x y z , P) (at level 200, x ident, y ident, z ident) : type_scope.
+Notation "∀ x y z u , P" :=
+ (forall x y z u , P) (at level 200, x ident, y ident, z ident, u ident) : type_scope.
+Notation "∀ x : t , P" :=
+ (forall x : t , P) (at level 200, x ident) : type_scope.
+Notation "∀ x y : t , P" :=
+ (forall x y : t , P) (at level 200, x ident, y ident) : type_scope.
+Notation "∀ x y z : t , P" :=
+ (forall x y z : t , P) (at level 200, x ident, y ident, z ident) : type_scope.
+Notation "∀ x y z u : t , P" :=
+ (forall x y z u : t , P) (at level 200, x ident, y ident, z ident, u ident) : type_scope.
+
+Notation "∃ x , P" := (exists x , P) (at level 200, x ident) : type_scope.
+Notation "∃ x : t , P" := (exists x : t, P) (at level 200, x ident) : type_scope.
+
+Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope.
+Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope.
+(* DOES NOT WORK
+Notation "x → y" := (x -> y) (at level 90, right associativity): type_scope.
+*)
+Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope.
+Notation "⌉ x" := (~x) (at level 75, right associativity) : type_scope.
-Notation "∃ x : t , P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
-Notation "x ∨ y" := (x \/ y) (at level 1, y at level 10).
-Notation "x ∧ y" := (x /\ y) (at level 1, y at level 10).
-Notation "x → y" := (x -> y) (at level 1, y at level 10).
-Notation "x ↔ y" := (x <-> y) (at level 1, y at level 10).
-Notation "⌉ x" := (~x) (at level 1, x at level 10).
(* Abstraction *)
+(* Not nice
Notation "'λ' x : T , y" := ([x:T] y) (at level 1, x,T,y at level 10).
Notation "'λ' x := T , y" := ([x:=T] y) (at level 1, x,T,y at level 10).
+*)
(* Arithmetic *)
-Notation "x ≤ y" := (le x y) (at level 3, y at level 10).
-Notation "x ≥ y" := (ge x y) (at level 3, y at level 10).
+Notation "x ≤ y" := (le x y) (at level 70, no associativity).
+Notation "x ≥ y" := (ge x y) (at level 70, no associativity).
+
+(* test *)
+(*
+Goal ∀ x, (∃ y , x ≥ y + 1) ∨ x ≤ 0.
+*)
-(* Require ZArith.
- Notation "x ≤ y" := (Zle x y) (at level 1, y at level 10).*)
+(* Integer Arithmetic *)
+(* TODO
+Notation "x ≤ y" := (Zle x y) (at level 1, y at level 10).
+*)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 01:29:22 +0000