[PATCH] formal: Trivial typo fixes

[PATCH] formal: Trivial typo fixes

[Akira Yokosawa]

From aefb442330115d2af25f532fcd725ed4c06e6908 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Tue, 19 Jul 2016 23:30:18 +0900
Subject: [PATCH] formal: Trivial typo fixes

Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
 formal/formal.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/formal/formal.tex b/formal/formal.tex
index 0e5fef3..ed9d7a3 100644
--- a/formal/formal.tex
+++ b/formal/formal.tex
@@ -126,7 +126,7 @@ The larger overarching software construct is of course validated by testing.
 	because the rate of change is just too great.
 	Furthermore, although the L4 microkernel is a large software
 	artifact from the viewpoint of formal verification, it is tiny
-	compared to the a great number of projects, including LLVM,
+	compared to a great number of projects, including LLVM,
 	gcc, the Linux kernel, Hadoop, MongoDB, and a great many others.

 	Although formal verification is finally starting to show some
@@ -171,4 +171,4 @@ All else being equal, a simpler implementation is much better than
 a mechanical proof for a complex implementation!

 And the open challenge to those working on formal verification techniques
-and systems is prove this summary wrong!
+and systems is to prove this summary wrong!
-- 
1.9.1

Re: [PATCH] formal: Trivial typo fixes

[Akira Yokosawa]

On 2016/07/19 23:42 +0900, Akira Yokosawa wrote:

Hi Paul,

These are typos I noticed while reading recently updated part in "formal/formal.tex".

>  	Furthermore, although the L4 microkernel is a large software
>  	artifact from the viewpoint of formal verification, it is tiny
> -	compared to the a great number of projects, including LLVM,
> +	compared to a great number of projects, including LLVM,

Here, "the" and "a" are redundant. I removed "the", because I have no idea
how many projects are there in this context.

>  	gcc, the Linux kernel, Hadoop, MongoDB, and a great many others.
>  
>  	Although formal verification is finally starting to show some
> @@ -171,4 +171,4 @@ All else being equal, a simpler implementation is much better than
>  a mechanical proof for a complex implementation!
>  
>  And the open challenge to those working on formal verification techniques
> -and systems is prove this summary wrong!
> +and systems is to prove this summary wrong!
> 

This seems a trivial one.

                                                Thanks, Akira

Re: [PATCH] formal: Trivial typo fixes

[Paul E. McKenney]

On Tue, Jul 19, 2016 at 11:42:13PM +0900, Akira Yokosawa wrote:
> >From aefb442330115d2af25f532fcd725ed4c06e6908 Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Tue, 19 Jul 2016 23:30:18 +0900
> Subject: [PATCH] formal: Trivial typo fixes
> 
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>

Thank you!

I queued both this and the quick-quiz explanation.  I wordsmithed
the explanation as shown below.

							Thanx, Paul

> ---
>  formal/formal.tex | 4 ++--
>  1 file changed, 2 insertions(+), 2 deletions(-)
> 
> diff --git a/formal/formal.tex b/formal/formal.tex
> index 0e5fef3..ed9d7a3 100644
> --- a/formal/formal.tex
> +++ b/formal/formal.tex
> @@ -126,7 +126,7 @@ The larger overarching software construct is of course validated by testing.
>  	because the rate of change is just too great.
>  	Furthermore, although the L4 microkernel is a large software
>  	artifact from the viewpoint of formal verification, it is tiny
> -	compared to the a great number of projects, including LLVM,
> +	compared to a great number of projects, including LLVM,
>  	gcc, the Linux kernel, Hadoop, MongoDB, and a great many others.
> 
>  	Although formal verification is finally starting to show some
> @@ -171,4 +171,4 @@ All else being equal, a simpler implementation is much better than
>  a mechanical proof for a complex implementation!
> 
>  And the open challenge to those working on formal verification techniques
> -and systems is prove this summary wrong!
> +and systems is to prove this summary wrong!
> -- 
> 1.9.1
> 

------------------------------------------------------------------------

commit c2260df4e50e2384d99713f8e07b62275e1aa7b2
Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Date:   Tue Jul 19 08:08:08 2016 -0700

    Wordsmith switching between quick-quiz questions and answers
    
    Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

diff --git a/howto/howto.tex b/howto/howto.tex
index 68ed47d919b0..efb570c9d066 100644
--- a/howto/howto.tex
+++ b/howto/howto.tex
@@ -209,12 +209,12 @@ Here are a few possible strategies:

 Note that as of mid-2016 the quick quizzes are hyperlinked
 to the answers and vice versa.
-Click either the ``Quick Quiz'' headings or the small squares
-to move back and forth between quiz and answer.
-Also note that the white squares at the end of answers are
-linked to the black squares at the end of quizzes.
-If you want to continue reading text after the end of quizzes,
-white squares would be of your choice.
+Click either the ``Quick Quiz'' heading or the small black square
+to move to the beginning of the answer.
+From the answer, click on the heading or the small black square to
+move to the beginning of the quiz, or, alternatively, click on the
+small white square at the end of the answer to move to the end of the
+corresponding quiz.
 } \QuickQuizEnd

 In short, if you need a deep

Re: [PATCH] formal: Trivial typo fixes

[Paul E. McKenney]

On Wed, Jul 20, 2016 at 12:08:29AM +0900, Akira Yokosawa wrote:
> On 2016/07/19 23:42 +0900, Akira Yokosawa wrote:
> 
> Hi Paul,
> 
> These are typos I noticed while reading recently updated part in "formal/formal.tex".
> 
> >  	Furthermore, although the L4 microkernel is a large software
> >  	artifact from the viewpoint of formal verification, it is tiny
> > -	compared to the a great number of projects, including LLVM,
> > +	compared to a great number of projects, including LLVM,
> 
> Here, "the" and "a" are redundant. I removed "the", because I have no idea
> how many projects are there in this context.
> 
> >  	gcc, the Linux kernel, Hadoop, MongoDB, and a great many others.
> >  
> >  	Although formal verification is finally starting to show some
> > @@ -171,4 +171,4 @@ All else being equal, a simpler implementation is much better than
> >  a mechanical proof for a complex implementation!
> >  
> >  And the open challenge to those working on formal verification techniques
> > -and systems is prove this summary wrong!
> > +and systems is to prove this summary wrong!
> > 
> 
> This seems a trivial one.

Agreed on both, pulled and pushed.  And thank you for your careful
review and the fixes!

							Thanx, Paul