% -*- TeX:EN -*- %%% ==================================================================== %%% @LaTeX-file qedeq_development_concept %%% Generated from http://www.qedeq.org/0_04_07/doc/project/qedeq_development_concept.xml %%% Generated at 2013-05-24 06:25:44.246 %%% ==================================================================== %%% Permission is granted to copy, distribute and/or modify this document %%% under the terms of the GNU Free Documentation License, Version 1.2 %%% or any later version published by the Free Software Foundation; %%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. \documentclass[a4paper,german,10pt,twoside]{book} \usepackage[english]{babel} \usepackage{makeidx} \usepackage{amsmath,amsthm,amssymb} \usepackage{color} \usepackage{xr} \usepackage{tabularx} \usepackage[bookmarks=true,bookmarksnumbered,bookmarksopen, unicode=true,colorlinks=true,linkcolor=webgreen, pagebackref=true,pdfnewwindow=true,pdfstartview=FitH]{hyperref} \definecolor{webgreen}{rgb}{0,.5,0} \usepackage{epsfig,longtable} \usepackage{graphicx} \usepackage[all]{hypcap} \newtheorem{thm}{Theorem} \newtheorem{cor}[thm]{Corollary} \newtheorem{lem}[thm]{Lemma} \newtheorem{prop}[thm]{Proposition} \newtheorem{ax}{Axiom} \newtheorem{rul}{Rule} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{idefn}[defn]{Initial Definition} \theoremstyle{remark} \newtheorem{rem}[thm]{Remark} \newtheorem*{notation}{Notation} \addtolength{\textheight}{7\baselineskip} \addtolength{\topmargin}{-5\baselineskip} \setlength{\parindent}{0pt} \frenchspacing \sloppy \makeindex \title{\textbf{Hilbert~II} \\ \vspace*{1cm} Presentation of \\ Formal Correct \\ Mathematical Knowledge \\ \vspace*{1cm} Development Concept} \author{ Michael Meyling } \begin{document} \maketitle \setlength{\parskip}{5pt plus 2pt minus 1pt} \mbox{} \vfill \par The source for this document can be found here: \par \url{http://www.qedeq.org/0_04_07/doc/project/qedeq_development_concept.xml} \par Copyright by the authors. All rights reserved. \par If you have any questions, suggestions or want to add something to the list of modules that use this one, please send an email to the address \href{mailto:mime@qedeq.org}{mime@qedeq.org} \par The authors of this document are: Michael Meyling \href{mailto:michael@meyling.com}{michael@meyling.com} \par Used other QEDEQ modules: \par \par \textbf{b} qedeq\_basic\_concept \url{http://www.qedeq.org/0_04_07/doc/project/qedeq_basic_concept_en.pdf} \par \textbf{f} qedeq\_logic\_language \url{http://www.qedeq.org/0_04_07/doc/project/qedeq_logic_language_en.pdf} \setlength{\parskip}{0pt} \tableofcontents \setlength{\parskip}{5pt plus 2pt minus 1pt} \chapter{General Information\label{ch:general}} \label{chapter1} \hypertarget{chapter1}{} The project \textbf{Hilbert~II} deals with presentation and documentation of mathematical knowledge. Therefore \textbf{Hilbert~II} supplies a program suite for the realization of the related tasks. Also the documentation of basic mathematical theories is a main purpose of this project. \par This document contains a description of the development concepts of \textbf{Hilbert~II}. You should have knowledge of the basic~concept~\url{http://www.qedeq.org/0_04_07/doc/project/qedeq_basic_concept_en.pdf}~\cite{b} and the logic~language~\url{http://www.qedeq.org/0_04_07/doc/project/qedeq_logic_language_en.pdf}~\cite{f} already. \section{Basics} \label{chapter1_section1} \hypertarget{chapter1_section1}{} Reference implementation in java. Executable as Java 1.4.2 GUI application. The application executes standalone or via Java Webstart. \par Currently the development is done within eclipse. Source Control Mangagement system is subversion. \par We have a hudson CI server. The release build is also done by that server. Main build script language is ant which runs under Java 1.6. We also produce maven POMs and trigger maven builds. Currently the kernel jars are also available via maven central. \section{Setup Development Environment} \label{chapter1_section2} \hypertarget{chapter1_section2}{} We need java and eclipse. Install java. For example via \url{http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html} \par Change Install eclipse. For example via \url{http://eclipse.org/downloads/packages/eclipse-ide-java-ee-developers/junosr2} \par Under 'Window/Preferences/General/Workspace' change 'Text file encoding' to 'Other: UTF-8' and 'New text file line delimiter' to 'Other: Unix'. \par Under 'Window/Preferences/General/Editors/Text Editors' mark box 'Insert spaces for tabs'. Also activate 'Show print margin' and set 'Print margin column' to 120. \par 'Help/Install New Software...' Add 'svn' '\url{http://subclipse.tigris.org/update_1.6.x}' install svn. \par 'Window/Open Perspective/Other/SVN Repository Exploring' 'Add SVN Repository' with URL '\url{https://svn.code.sf.net/p/pmii/code/trunk}'. Browse the new repository and check out all direct subnodes as projects.\footnote{This should be: QedeqBase QedeqBaseTest, QedeqBuild, QedeqDoc, QedeqGuiSe, QedeqKernelBo, QedeqKernelBoTest, QedeqKernelSe, QedeqKernelSeTest, QedeqKernelXml, QedeqKernelXmlTest, QedeqLib} \section{Architecture} \label{chapter1_section3} \hypertarget{chapter1_section3}{} We have four tiers that are encapsulated in different eclipse projects. \subsection{QedeqBase } Project independent basis classes. \subsection{QedeqKernelSe } Project dependent basis classes. Contains value objects. \subsection{QedeqKernelBo } Here the kernel services can be called. \subsection{QedeqKernelXml } We speak XML here. Parsing of XML files and BO serialization is the domain of this package. %% end of chapter General Information\label{ch:general} \backmatter \begin{thebibliography}{99} \addcontentsline{toc}{chapter}{Bibliography} %% Used other QEDEQ modules: \bibitem{b} qedeq\_basic\_concept \url{http://www.qedeq.org/0_04_07/doc/project/qedeq_basic_concept_en.pdf} \bibitem{f} qedeq\_logic\_language \url{http://www.qedeq.org/0_04_07/doc/project/qedeq_logic_language_en.pdf} %% Other references: \end{thebibliography} \addcontentsline{toc}{chapter}{\indexname} \printindex \end{document}