Commit c4d770c2 authored by François Bobot's avatar François Bobot
Browse files

[SRC] use markdown

parent 2569331f
PKG tyxml
PKG lambdoc
B _build
S .
\ No newline at end of file
......@@ -17,10 +17,10 @@ clean:
# --- Compilation
# --------------------------------------------------------------------------
PREFIX?=/usr/local
PACKAGES=tyxml
PACKAGES=tyxml lambdoc
FLAGS= \
-cflags -w,PSUZL+7,-warn-error,PSUZL+7 \
-use-ocamlfind -tag debug \
-use-ocamlfind -tag debug -tag thread \
$(addprefix -package ,$(PACKAGES))
ifeq ($(DEVEL),YES)
......
......@@ -22,9 +22,23 @@ let page p b =
(head (title (pcdata ("SOPRANO: "^p.long_title)))
[
meta ~a:[a_charset "utf-8"] ();
link ~rel:[`Stylesheet] ~href:"css/main.css" ()
link ~rel:[`Stylesheet] ~href:"css/main.css" ();
link ~rel:[`Stylesheet] ~href:"css/lambdoc.css" ();
])
(body ([header;content;menu])) in
Html5.P.print ~output:print_string html
type a_remplir = ARemplir (** For the squeleton *)
(** {2 Markdown} *)
module Lambdoc_writer = Lambdoc_write_html5.Make_simple (struct
include Html5.M
module Svg = Svg.M
end)
let md s : [> Html5_types.div ] Html5.M.elt =
let doc = Lambdoc_read_markdown.Simple.ambivalent_from_string s in
let xdoc = Lambdoc_writer.write_ambivalent doc in
( xdoc :
(Html5_types.div Html5.M.elt) :> [> Html5_types.div ] Html5.M.elt)
(** {2 For the squeleton } *)
type a_remplir = ARemplir
......@@ -6,7 +6,7 @@ let p_pcdata txt = p [pcdata txt]
let () = Generate.page main [
div ~a:[a_style "align:justify"] [
p_pcdata "
md "
Modern societies crucially rely on digital infrastructures, and it
is becoming clear that high-quality software can be obtained only
with the help of proper software verification tools. Today most
......@@ -15,12 +15,10 @@ These solvers, however, do not fill the current and future needs for
verification: lack of satisfying model generation, lack of
reasoning on difficult theories (e.g. floating-point arithmetic),
lack of extensibility for specific or new needs.
The SOPRANO project aims at solving these problems and preparing the next
generation of verification-oriented solvers by gathering experts
from academia and industry.";
from academia and industry.
p_pcdata "
We will design a new framework for the
cooperation of solvers, focused on model generation and borrowing
principles from SMT (current standard) and CP (well-known in
......@@ -35,9 +33,8 @@ industry-relevant and hard-to-solve theories. The third objective
is to implement these results in a new open-source platform. The
fourth objective is to ensure industrial-adequacy of the techniques
and tools developed through periodical evaluations
from the industrial partners.";
from the industrial partners.
p_pcdata "
Our main approach is to combine principles coming from both SMT
and CP. Roughly speaking, we seek to add to SMT the extensibility
of CP and its native handling of domains, and to CP the elegant
......@@ -48,9 +45,8 @@ a privileged status. We want to explore how to break this
privileged status, in order to allow theory
solvers to contribute more directly to each part of the solving
process. For that, we will develop a notion of first-class domain
and first-class conflict analysis.";
and first-class conflict analysis.
p_pcdata "
The major results of the project includes scientific,
technological, and industrial benefits.
The project has the potential to deliver significant breakthroughs
......@@ -68,8 +64,8 @@ OCamlPro and AdaCore, the industrial partners, will take full
advantage of the project to improve their lines of products and
services. Finally, traditional industrial partners of CEA and
UPSud will directly benefit from improvements of the verification
tools of the project members.";
p_pcdata "
tools of the project members.
The Consortium is composed of CEA (software verification tools and
CP solving), University of Paris-Sud (SMT solving and
floating-point theory), Inria Rennes (CP solving, floating-point theory),
......
/* html, body, div, span, applet, object, iframe, h1, h2, h3, h4, h5, h6, p, blockquote, pre, a, abbr, acronym, address, big, cite, code, del, dfn, em, font, img, ins, kbd, q, s, samp, small, strike, strong, sub, sup, tt, var, dl, dt, dd, ol, ul, li, fieldset, form, label, legend, table, caption, tbody, tfoot, thead, tr, th, td, button */
/* { */
/* margin: 0; */
/* padding: 0; */
/* border: 0; */
/* outline: 0; */
/* font-weight: inherit; */
/* font-style: inherit; */
/* font-size: 100%; */
/* font-family: inherit; */
/* vertical-align: baseline; */
/* } */
/* :focus */
/* { */
/* outline: 0; */
/* } */
/* body */
/* { */
/* line-height: 1; */
/* color: black; */
/* background: white; */
/* } */
/* ol, ul */
/* { */
/* list-style: none; */
/* } */
/* table */
/* { */
/* border-collapse: separate; */
/* border-spacing: 0; */
/* } */
/* caption, th, td */
/* { */
/* text-align: left; */
/* font-weight: normal; */
/* } */
.doc_bold
{
font-weight: bold;
}
.doc_emph
{
font-style: italic;
}
.doc_code
{
font-family: "DejaVu Sans Mono", "Courier New", "Courier", monospace;
font-weight: bold;
color: #333;
}
.doc_caps
{
font-variant: small-caps;
}
.doc_ins
{
text-decoration: underline;
color: #090;
}
.doc_del
{
text-decoration: line-through;
color: #900;
}
.doc_sup
{
vertical-align: 0.3em;
}
.doc_sub
{
vertical-align: -0.1em;
}
.doc_mbox
{
white-space: nowrap;
}
.doc_lnk
{
text-decoration: none;
color: #009;
}
.doc_see
{
margin-left: 0.25em;
vertical-align: 0.3em;
font-size: 13px;
color: #009;
}
.doc_cite
{
margin-left: 0.25em;
color: #009;
}
.doc_par
{
margin: 0.5em 0;
text-align: justify;
}
.doc_par:first-child
{
margin-top: 0;
}
.doc_par:last-child
{
margin-bottom: 0;
}
.doc_class_initial:first-letter
{
float: left;
margin-right: 0.15em;
font-weight: bold;
font-size: 3.5em;
text-transform: capitalize;
color: #501;
}
.doc_par + .doc_par:not(.doc_class_initial)
{
text-indent: 1em;
}
.doc_par.doc_class_indent:not(.doc_class_initial)
{
text-indent: 1em;
}
.doc_par.doc_class_noindent
{
text-indent: 0 !important;
}
.doc_itemize, .doc_enumerate, .doc_description
{
margin: 1em 0 1em 2em;
}
.doc_itemize:first-child, .doc_enumerate:first-child, .doc_description:first-child
{
margin-top: 0;
}
.doc_itemize:last-child, .doc_enumerate:last-child, .doc_description:last-child
{
margin-bottom: 0;
}
.doc_itemize > .doc_item, .doc_enumerate > .doc_item
{
margin: 0.5em 0;
}
.doc_description > dt.doc_item
{
margin: 0.5em 0 0.25em -1.5em;
font-weight: bold;
color: #501;
}
.doc_itemize
{
list-style: disc outside;
}
.doc_enumerate
{
list-style: decimal outside;
}
.doc_class_none
{
list-style-type: none;
}
.doc_class_disc
{
list-style-type: disc;
}
.doc_class_circle
{
list-style-type: circle;
}
.doc_class_square
{
list-style-type: square;
}
.doc_class_decimal
{
list-style-type: decimal;
}
.doc_class_lower-roman
{
list-style-type: lower-roman;
}
.doc_class_upper-roman
{
list-style-type: upper-roman;
}
.doc_class_lower-alpha
{
list-style-type: lower-alpha;
}
.doc_class_upper-alpha
{
list-style-type: upper-alpha;
}
.doc_qanda
{
margin: 1em 0;
}
.doc_qanda:first-child
{
margin-top: 0;
}
.doc_qanda:last-child
{
margin-bottom: 0;
}
dt.doc_question, dt.doc_answer
{
display: block;
float: left;
margin-right: 0.5em;
font-weight: bold;
font-variant: small-caps;
}
dt.doc_answer
{
margin-left: 1.5em;
}
dt.doc_answer:before
{
display: block;
float: left;
margin-left: -0.75em;
height: 0;
line-height: 1em;
font-family: "Georgia", serif;
font-weight: bold;
font-variant: normal;
font-size: 1.8em;
quotes: "\201c" "\201d";
content: open-quote;
color: #501;
}
dd.doc_question
{
margin: 0.5em 0;
}
dd.doc_answer
{
margin: 0.5em 0 1em 1.5em;
}
.doc_question
{
color: #501;
}
.doc_verse
{
clear: both;
margin: 1.5em 1em;
text-align: center;
}
.doc_verse:first-child
{
margin-top: 0;
}
.doc_verse:last-child
{
margin-bottom: 0;
}
.doc_verse_aux
{
display: inline-block;
font-style: italic;
}
.doc_verse_aux > .doc_par
{
text-indent: 0 !important;
}
.doc_quote
{
clear: both;
margin: 1.5em 1em;
padding-left: 0.75em;
border-left: 2px dotted #501;
color: #444;
}
.doc_quote:first-child
{
margin-top: 0;
}
.doc_quote:last-child
{
margin-bottom: 0;
}
.doc_mathblk
{
clear: both;
margin: 1em 1em;
text-align: center;
}
.doc_mathblk:first-child
{
margin-top: 0;
}
.doc_mathblk:last-child
{
margin-bottom: 0;
}
.doc_src_main
{
clear: both;
margin: 1.5em 1em;
font-size: 13px;
font-family: "DejaVu Sans Mono", "Courier New", "Courier", monospace;
line-height: 1.8em;
overflow: auto;
}
.doc_src_main:first-child
{
margin-top: 0;
}
.doc_src_main:last-child
{
margin-bottom: 0;
}
.doc_src_nums
{
float: left;
margin-right: 1em;
border-right: 1px solid #666;
white-space: normal;
font-weight: bold;
}
.doc_src_code
{
white-space: normal;
}
.doc_src_line
{
display: block;
white-space: pre;
height: 1.8em;
padding: 0 1em;
}
.doc_src_dummy
{
display: none;
height: 0;
padding: 0.3em 0;
}
.doc_src_Kwd
{
color: #0000ff;
font-weight: bold;
}
.doc_src_Type
{
color: #007f00;
}
.doc_src_Utyp
{
color: #007f7f;
}
.doc_src_Str
{
color: #ff0000;
}
.doc_src_Rex
{
color: #ff9f00;
}
.doc_src_Sch
{
color: #ffbfcf;
}
.doc_src_Com
{
color: #9f2f2f;
font-style: italic;
}
.doc_src_Num
{
color: #7f007f;
}
.doc_src_Prep
{
color: #00007f;
font-weight: bold;
}
.doc_src_Sym
{
color: #7f0000;
}
.doc_src_Fun
{
color: #000000;
font-weight: bold;
}
.doc_src_Cbrk
{
color: #ff0000;
}
.doc_src_Pvar
{
color: #00007f;
}
.doc_src_Pfun
{
color: #00007f;
font-weight: bold;
}
.doc_src_Clas
{
color: #007f7f;
}
.doc_src_Line
{
color: #000000;
}
.doc_src_Url
{
color: #0000ff;
text-decoration: underline;
}
.doc_src_Date
{
color: #0000ff;
font-weight: bold;
}
.doc_src_Time
{
color: #00007f;
font-weight: bold;
}
.doc_src_File
{
color: #00007f;
font-weight: bold;
}
.doc_src_Ip
{
color: #007f00;
}
.doc_src_Name
{
color: #007f00;
}
.doc_src_Var
{
color: #007f00;
}
.doc_src_Ital
{
color: #007f00;
font-style: italic;
}
.doc_src_Bold
{
color: #007f00;
font-weight: bold;
}
.doc_src_Undr
{
color: #007f00;
text-decoration: underline;
}