Commit 35860585 authored by Guillaume Melquiond's avatar Guillaume Melquiond

New release.

parent eaa9655d
Version 2.5.0:
- iter_pos?
TODO
- new definition of the ulp with a nice ulp(0)
- changed named, generalized and added lemmas in Fcore_ulp
- defined a predecessor and successor on both positive, negative and
zero values (the previous pred has been renamed pred_pos)
- ensured compatibility with both Coq 8.4 and 8.5
(Flocq now provides its own version of iter_pos)
- redefined ulp, so that ulp(0) is meaningful
- renamed, generalized, and added lemmas in Fcore_ulp
- extended predecessor and successor to nonpositive values
(the previous definition of pred has been renamed pred_pos)
- removed some hypotheses on lemmas of Fprop_relative
- More examples have been added
* Average: proof on Sterbenz's average and correctly-rounded average
TODO
* Cody_Waite
* Compute: effective FP computation inside Coq with an example of
(sqr (sqrt x)) in radix 5 and precision 3.
* Division_u16
* Triangle: Kahan's algorithm for the area of a triangle
- added more examples
. Average: proof on Sterbenz's average and correctly-rounded average
. Cody_Waite: Cody & Waite's approximation of exponential
. Compute: effective FP computations with an example of sqrt(sqr(x))
in radix 5 and precision 3
. Division_u16: integer division using floating-point FMA
. Triangle: Kahan's algorithm for the area of a triangle
Version 2.4.0:
- moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
......
AC_INIT([Flocq], [2.4.0],
AC_INIT([Flocq], [2.5.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
......
......@@ -348,8 +348,8 @@ https://github.com/apenwarr/redo for an implementation and some comprehensive do
\section sec-licensing Licensing
@author Guillaume Melquiond
@version 0.11
@date 2012-2013
@version 0.12
@date 2012-2014
@copyright
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
......@@ -2063,7 +2063,7 @@ static bool still_need_rebuild(std::string const &target)
/**
* Handle job completion.
*/
static void complete_job(int job_id, bool success)
static void complete_job(int job_id, bool success, bool started = true)
{
DEBUG << "Completing job " << job_id << '\n';
job_map::iterator i = jobs.find(job_id);
......@@ -2071,14 +2071,15 @@ static void complete_job(int job_id, bool success)
string_list const &targets = i->second.rule.targets;
if (success)
{
if (show_targets) std::cout << "Finished";
bool show = show_targets && started;
if (show) std::cout << "Finished";
for (string_list::const_iterator j = targets.begin(),
j_end = targets.end(); j != j_end; ++j)
{
update_status(*j);
if (show_targets) std::cout << ' ' << *j;
if (show) std::cout << ' ' << *j;
}
if (show_targets) std::cout << std::endl;
if (show) std::cout << std::endl;
}
else
{
......@@ -2086,9 +2087,15 @@ static void complete_job(int job_id, bool success)
for (string_list::const_iterator j = targets.begin(),
j_end = targets.end(); j != j_end; ++j)
{
status[*j].status = Failed;
std::cerr << ' ' << *j;
remove(j->c_str());
update_status(*j);
status_e &s = status[*j].status;
if (s != Uptodate)
{
DEBUG << "Removing " << *j << '\n';
remove(j->c_str());
}
s = Failed;
}
std::cerr << std::endl;
}
......@@ -2372,7 +2379,7 @@ static void complete_request(client_t &client, bool success)
assert(i != jobs.end());
if (still_need_rebuild(i->second.rule.targets.front()))
run_script(client.job_id, i->second);
else complete_job(client.job_id, true);
else complete_job(client.job_id, true, false);
}
else complete_job(client.job_id, false);
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment