Offer syntax and semantics checks separately

[patritzenfeld]

The package exposes grade, which does both at once. We would like to accurately label the steps in Autotool, so the compile checks needs to be separated from Hlint feedback and test execution.

[jvoigtlaender]

Arguably, Hlint could be considered to be about "syntax", respectively lumped in with the compile checks.

[jvoigtlaender]

I see that you have started moving checks around. Their order was quite deliberately tuned at some point, and there were non-obvious reasons for „this should come before that“ etc. (But I don’t remember all the arguments, just that it took a while to settle.)

Ideally, the separation now would be a clean cut in two, without reordering. Even if that would mean for the moment my suggestion above about letting hlint be conceptually part of syntax checking cannot be enacted.

[jvoigtlaender]

Actually, for the concrete use case envisioned for the semester (providing sample solutions after the submission deadline), the first change would seem to be to move all current checks from the „semantics“ to the „syntax“ phase, because also all the test suite should run in the pre-deadline phase (only the display of sample solution being delayed by the restriction setting on Autotool).

Subsequently, maybe with a view toward exam usage, a config setting could be introduced by which a „splt point“ is set up to which the feedback is included into the „syntax phase“.

[patritzenfeld]

I was not aware that we want to introduce restricted mode for Haskell tasks (but of course that makes sense if we want to display a sample solution). This might cause a different problem:

In Autotool, we currently have no options to display non-terminating output in the syntax phase. So that means we cannot display optional Hlint hints, except if there are also required ones if everything is moved to syntax right now. Purely "warning" style output will only become visible after the deadline if we restrict the task. This will require additional work in Autotool (introducing some new persisted data type and editing the settings menu)

[jvoigtlaender]

I'm not sure what this means:

display non-terminating output

[patritzenfeld]

Any output that calls reject, rejectPre, etc. in the Autotool Output type or toAbort in output-blocks short circuits the reporter. What I meant is output that does not contain a call to such a function, thus resulting in "Good Syntax".

[jvoigtlaender]

Okay, so the "syntax checker" cannot output positive information? Its output will only be visible if it has decided to reject the input?

I didn't know that (and have made suggestions under an opposite assumption, such as here: fmidue/flex-tasks#203).

Let's not go into any changes on the Autotool side, instead work with what the API is there.

That probably means the split now should be at this line:

haskell-template-task/src/Haskell/Template/Task.hs

Line 414 in c7cd07f

void $ getHlintFeedback inform config dirname solutionFile False

i.e., leaving the Hlint suggestions-only to the "after the deadline" phase. That's okay.

What about the line before that,

haskell-template-task/src/Haskell/Template/Task.hs

Line 413 in c7cd07f

compileWithArgsAndCheck dirname reject inform config noTest False

Does it also only make sense in the after-deadline phase then? It does contain a reject occurrence. But can that one actually fire? If the reject from that line becomes called, would that case have already triggered in the preceding line

haskell-template-task/src/Haskell/Template/Task.hs

Line 408 in c7cd07f

compileWithArgsAndCheck dirname reject undefined config noTest True

as well?

Probably it would be good, for knowing what the "stages" actually are here, to first write in-the-code comments about what each line in

haskell-template-task/src/Haskell/Template/Task.hs

Lines 402 to 414 in c7cd07f

	compilation <- liftIO $ runInterpreter (compiler dirname config noTest)
	checkResult reject compilation reject Nothing $ const $ return ()
	when (runIdentity $ allowModifying config) $ do
	compilationWithTests <- liftIO $ runInterpreter $
	compiler dirname config modules
	checkResult reject compilationWithTests signatureError Nothing $ const $ return ()
	compileWithArgsAndCheck dirname reject undefined config noTest True
	void $ getHlintFeedback rejectWithHint config dirname solutionFile True
	matchTemplate reject config 2 exts template submission
	result <- liftIO $ runInterpreter (interpreter dirname config modules)
	checkResult reject result reject Nothing $ handleCounts reject inform
	compileWithArgsAndCheck dirname reject inform config noTest False
	void $ getHlintFeedback inform config dirname solutionFile False

is actually doing/checking.

[patritzenfeld]

I've added comments for the steps in the dev branch.

What about the line before that,

compileWithArgsAndCheck dirname reject inform config noTest False
Does it also only make sense in the after-deadline phase then? It does contain a reject occurrence. But can that one actually fire? If the reject from that line becomes called, would that case have already triggered in the preceding line

compileWithArgsAndCheck dirname reject undefined config noTest True
as well?

reject is passed as a "fail safe" in the first call. It is only used in case of an unexpected error during compilation (which should not be possible at this stage anyway, since we already compiled it earlier?)

haskell-template-task/src/Haskell/Template/Task.hs

Lines 511 to 532 in af764cd

	compileWithArgsAndCheck
	:: MonadIO m
	=> FilePath
	-> (Doc -> m a)
	-> (Doc -> m a)
	-> SolutionConfig
	-> [String]
	-> Bool
	-> m ()
	compileWithArgsAndCheck dirname reject inform config modules asError = unless (null ghcOpts) $ do
	ghcErrors <-
	liftIO $ unsafeRunInterpreterWithArgs ghcOpts (compiler dirname config modules)
	checkResult reject ghcErrors how howMany $ const $ return ()
	where
	makeOpts xs = ("-w":) $ ("-Werror=" ++) <$> xs
	ghcOpts = makeOpts $ msum (warnings config)
	(warnings, how) =
	if asError
	then (configGhcErrors, rejectWithHint)
	else (configGhcWarnings, inform)
	howMany = runIdentity $ configGhcLimit config
	rejectWithHint = reject . vcat . (: singleton rejectHint)

haskell-template-task/src/Haskell/Template/Task.hs

Lines 578 to 587 in af764cd

	checkResult reject result handleError mErrorLimit handleResult = case result of
	Right result' -> void $ handleResult result'
	Left (WontCompile msgs) -> void $ handleError $ string
	$ intercalate "\n" $ amount
	$ map (editFeedback . formatHyperlinks) $ filterWerrors msgs
	Left err -> void $ reject $
	vcat ["An unexpected error occurred.",
	"This is usually not caused by a fault within your solution.",
	"Please contact your lecturers, providing the following error message:",
	nest 4 $ string $ show err]

[jvoigtlaender]

which should not be possible at this stage anyway, since we already compiled it earlier?

If we are confident that the second compileWithArgsAndCheck shouldn't come with new "unexpected/catastrophic errors", the reject in

haskell-template-task/src/Haskell/Template/Task.hs

Line 430 in 2e3ccf6

compileWithArgsAndCheck dirname reject inform config noTest False

could be replaced by undefined? Or maybe just leave it as is, like the rejects a few lines above.

[jvoigtlaender]

A suggestion about the API:

Let the eval argument not have type

(forall a. m a -> (a -> m ()) -> (a -> m ()) -> IO (b, Maybe b)),

but instead

(m (m ()) -> IO (b, Maybe b)),

and replace the current call

haskell-template-task/src/Haskell/Template/Task.hs

Line 434 in 2e3ccf6

eval prepare syntax semantics

by:

  eval $ do
    params <- prepare
    syntax params
    return (semantics params)

The current usage

haskell-template-task/test/Haskell/Template/TaskSpec.hs

Lines 168 to 174 in 2e3ccf6

	let eval prepare syntax semantics = do
	(params,setupResult) <- runWriterT prepare
	syntaxResult <- execWriterT $ syntax params
	semanticsResult <- execWriterT $ semantics params
	pure (setupResult ++ syntaxResult, Just semanticsResult)
	(syntax,mSemantics) <- grade
	eval

would then become (with better variable names still to be chosen):

    let eval block = do
          (semanticsWithParams, setupAndSyntaxResults) <- runWriterT block
          semanticsResult <- execWriterT semanticsWithParams
          pure (setupAndSyntaxResults, Just semanticsResult)
    (syntax,mSemantics) <- grade
      eval

[jvoigtlaender]

After the proposed API change for grade/eval, the current use of functions prepare, syntax, semantics inside grade could be dialed back.

Instead, there would be again a "monolithic" do-block, in which first the prepare stuff is run and binds the various parameters like config etc.; then the two lists currently passed to sequence_ there would be joined into one list but splitAt a configurable point; and then the overall structure would be something like:

eval $ do
  ... the prepare stuff ...
  let (firstList, secondList) = splitAt somePoint 
    [
      all the checks
    ]
  sequence_ firstList
  return (sequence_ secondList)

[jvoigtlaender]

The offered splitting points could be:

• Compilation, after these:

  haskell-template-task/src/Haskell/Template/Task.hs

  Lines 409 to 421 in de1e4af

  	-- Reject if submission does not compile with provided hidden modules,
  	-- but without Test module.
  	do
  	compilation <- liftIO $ runInterpreter (compiler dirname config noTest)
  	checkResult reject compilation reject Nothing $ const $ return ()
  	,
  	-- Reject if submission does not compile with provided hidden modules.
  	-- This only runs when allowModifying is set to True in the config
  	-- and displays a custom message telling students not to change type signatures.
  	when (runIdentity $ allowModifying config) $ do
  	compilationWithTests <- liftIO $ runInterpreter $
  	compiler dirname config modules
  	checkResult reject compilationWithTests signatureError Nothing $ const $ return ()

• GhcErrors, after this:

  haskell-template-task/src/Haskell/Template/Task.hs

  Lines 423 to 424 in de1e4af

  	-- Reject if GHC warnings configured as errors are triggered by solution.
  	compileWithArgsAndCheck dirname reject undefined config noTest True

• HlintErrors, after this:

  haskell-template-task/src/Haskell/Template/Task.hs

  Lines 426 to 427 in de1e4af

  	-- Reject if HLint warnings configured as errors are triggered by solution.
  	void $ getHlintFeedback rejectWithHint config dirname solutionFile True

• TemplateMatch, after this:

  haskell-template-task/src/Haskell/Template/Task.hs

  Lines 429 to 430 in de1e4af

  	-- Reject on task template violations according to settings (modifying, adding, deleting).
  	matchTemplate reject config 2 exts template submission

• TestSuite, after this:

  haskell-template-task/src/Haskell/Template/Task.hs

  Lines 436 to 439 in de1e4af

  	-- Reject if test suite fails for submission.
  	do
  	result <- liftIO $ runInterpreter (interpreter dirname config modules)
  	checkResult reject result reject Nothing $ handleCounts reject inform

[jvoigtlaender]

The two occurrences of „(b, Maybe b)“ in the grade-type could still simply be „b“?

And is the polymorphism in the „(forall c . Doc -> m c)“ argument actually exploited? Or could it simply be typed „(Doc -> m ())“ instead?

[jvoigtlaender]

Well, maybe both of the current type choices questioned in the previous comment have documentary value. In fact, it might even make sense to monomorphise the b in „(b, Maybe b)“ to String?