Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Interactive merger! #44

Open
wants to merge 103 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
103 commits
Select commit Hold shift + click to select a range
516cc7e
[feature] Report rule applications to trace.
corwin-of-amber May 28, 2021
bc052b4
[feature] Trace derivation trail with vector args.
corwin-of-amber May 29, 2021
020b374
[ui] Parse & display derivation trail.
corwin-of-amber May 29, 2021
85f9f9e
[bugfix] Timeout displayed as "x seconds" in message.
corwin-of-amber May 29, 2021
ca0e219
[port] Newer JDK compat.
corwin-of-amber May 29, 2021
ccbe879
[refactor] Extracted some common logic from SubstL/R.
corwin-of-amber May 29, 2021
b12734b
[bugfix] Don't disable all loggers worldwide.
corwin-of-amber May 31, 2021
3a4e34e
[feature] Return result from `synthesizeFrom..` methods.
corwin-of-amber May 31, 2021
19cf684
[bugfix] Wrong dir name.
corwin-of-amber May 31, 2021
a6b98f2
[wip] Bare-bones synthesis server.
corwin-of-amber May 31, 2021
ce71b12
[wip] A very clunky server-side.
corwin-of-amber Jun 4, 2021
c2fc60a
[refactor] Moved all components to SFCs.
corwin-of-amber Jun 4, 2021
5bad3e8
[chore] Removed some npm warnings.
corwin-of-amber Jun 4, 2021
94e919e
[refactor] Changed client-server protocol to WebSockets.
corwin-of-amber Jun 4, 2021
6fe4f8f
[feature] Some interaction UI.
corwin-of-amber Jun 4, 2021
5a4c44c
[feature] Start with an empty trace then build incrementally.
corwin-of-amber Jun 5, 2021
189615f
[feature] More interaction.
corwin-of-amber Jun 5, 2021
e595617
[feature] Report synthesis result in JSON.
corwin-of-amber Jun 6, 2021
5a0bddd
[feature] Display derivation trail even for incomplete branches.
corwin-of-amber Jun 6, 2021
eb01707
[feature] Highlight current goal for interaction.
corwin-of-amber Jun 6, 2021
bf45f24
[feature] Accept spec from clients.
corwin-of-amber Jun 6, 2021
1da86e8
[feature] Bundle benchmarks in JSON.
corwin-of-amber Jun 8, 2021
0a2d3a7
[refactor] Wrapped UI in a root app component.
corwin-of-amber Jun 9, 2021
f72a20b
[ui] Display list of benchmarks on startup.
corwin-of-amber Jun 11, 2021
9e3407d
[ui] Reload button.
corwin-of-amber Jun 15, 2021
f098b92
[feature] Serialization additions.
corwin-of-amber Jun 17, 2021
9e5871d
[feature] Arbitary interactive expansion thingamabob.
corwin-of-amber Jun 17, 2021
71ce37d
[ui] Show spec in editor.
corwin-of-amber Jun 19, 2021
cf38b86
[bugfix] Pass the parameters to the server as well.
corwin-of-amber Jun 19, 2021
a3a1f51
[ui] Formatting stuff.
corwin-of-amber Jun 19, 2021
504ab7c
[deploy] Heroku support.
corwin-of-amber Jun 19, 2021
a22fc28
[feature] Interactive/automatic mode switch.
corwin-of-amber Jun 19, 2021
91e2c6e
[ui] Click to expand.
corwin-of-amber Jun 19, 2021
5ebb41f
Merge branch 'master' into interactive
nadia-polikarpova Jun 20, 2021
ca2647b
Minor
nadia-polikarpova Jun 20, 2021
ee966a6
First stab at simple rules
nadia-polikarpova Jun 21, 2021
aad7db4
Put simple under flag
nadia-polikarpova Jun 21, 2021
99620f4
Change read and write rule to follow slides
nadia-polikarpova Jun 21, 2021
005d77b
Comment out guided tests
nadia-polikarpova Jun 21, 2021
9b4376c
Replace uni mod theories with syntactic unification in simple synthes…
nadia-polikarpova Jun 23, 2021
9d590d7
Minor
nadia-polikarpova Jun 23, 2021
a62984b
[ui] Added proof mode switch.
corwin-of-amber Jun 24, 2021
a779885
[bugfix] Strip away params line.
corwin-of-amber Jun 24, 2021
2d159e0
[perf] Some throttling of messages in auto.
corwin-of-amber Jun 25, 2021
1ba98f2
Switched to `Simple` synthesis tactic (for server).
corwin-of-amber Jul 4, 2021
54925f4
[ui] Restore focus and report success.
corwin-of-amber Jul 5, 2021
0713d92
[bugfix] Multithread mayhem!
corwin-of-amber Jul 14, 2021
76a242d
[ui] Connection error reporting.
corwin-of-amber Jul 14, 2021
cd81904
[ui] Sane autoscroll.
corwin-of-amber Jul 14, 2021
fa0cd84
[qa] Added an sll-to-dll in-place example.
corwin-of-amber Jul 14, 2021
9328612
[wip] More serialization stuff.
corwin-of-amber Jul 16, 2021
8d47704
[feature] Report PickArg subst.
corwin-of-amber Jul 16, 2021
89f2c7a
[ui] Some panning and zooming.
corwin-of-amber Jul 16, 2021
14e6d86
[ui] Stabilized zoom.
corwin-of-amber Jul 19, 2021
844ef2b
[feature] Keep trace when switching mode.
corwin-of-amber Jul 20, 2021
1a4e428
[feature] Allow passing both syn and sus inputs to server.
corwin-of-amber Jul 21, 2021
3348113
Get rid of PickArg and use Pick instead
nadia-polikarpova Jul 21, 2021
51187f2
Merge branch 'interactive' of github.com:TyGuS/synsl into interactive
nadia-polikarpova Jul 21, 2021
0d4855b
Get rid of cardinalities in simple mode
nadia-polikarpova Jul 22, 2021
e883001
Make some rules non-invertible in simple mode (otherwise it is confus…
nadia-polikarpova Jul 22, 2021
c2192b7
[ui] Hide null cardinalities ("<0>").
corwin-of-amber Jul 22, 2021
1653ea4
[nits] Updated deps.
corwin-of-amber Jul 22, 2021
5997f07
[bugfix] Made `SearchTree` thread-local.
corwin-of-amber Jul 22, 2021
0deacc7
[ui] [feature] Show synthesized program.
corwin-of-amber Jul 22, 2021
12f680d
[interact] Set default timeout to 15sec.
corwin-of-amber Jul 22, 2021
f203b51
[interact] Change default open and close depth to 2
nadia-polikarpova Jul 22, 2021
3bffaf9
[ui] Simple-mode switch.
corwin-of-amber Jul 23, 2021
5f9f711
Merge remote-tracking branch 'refs/remotes/origin/interactive' into i…
corwin-of-amber Jul 23, 2021
731d3f7
[tut] Bundle files from tutorial repo.
corwin-of-amber Jul 23, 2021
61e4b64
[feature] Basic syntax highlighting.
corwin-of-amber Jul 23, 2021
538b75f
[ui] Highlight active benchmark.
corwin-of-amber Jul 23, 2021
f10b4b2
[bugfix] Some crossfire between docs.
corwin-of-amber Jul 23, 2021
c706aa5
[feature] [ui] Start/stop buttons.
corwin-of-amber Jul 23, 2021
2f87f29
Updated tutorial files.
corwin-of-amber Jul 23, 2021
4b2e725
Playing with tutorial examples
nadia-polikarpova Jul 23, 2021
543f2b5
Merge branch 'interactive' of github.com:TyGuS/synsl into interactive
nadia-polikarpova Jul 23, 2021
42037f9
Throwing timeout exception as opposed to synthesis failed on timeout
nadia-polikarpova Jul 23, 2021
9f528ca
[bugfix] Moved the Memo to TLS as well.
corwin-of-amber Jul 23, 2021
936e22b
[tut] Hide solutions by default.
corwin-of-amber Jul 23, 2021
c247ded
[ui] Sticky notifications.
corwin-of-amber Jul 23, 2021
bed814c
Rename pick rule back
nadia-polikarpova Jul 23, 2021
3a54b51
Merge branch 'interactive' of github.com:TyGuS/synsl into interactive
nadia-polikarpova Jul 23, 2021
a33c206
[ui] Show call info for suspended calls.
corwin-of-amber Jul 23, 2021
e572a6b
[ui] Show companion goal id in call.
corwin-of-amber Jul 23, 2021
ed1e0cf
[ui] Some additional styling.
corwin-of-amber Jul 23, 2021
f966a3e
[bugfix] Use unique ids for goals.
corwin-of-amber Jul 23, 2021
7141c7b
[ui] Better styling of node labels.
corwin-of-amber Jul 24, 2021
f45a572
[ui] Style operators.
corwin-of-amber Jul 24, 2021
c2083a6
[nit] Reset global counter on each task.
corwin-of-amber Jul 27, 2021
261011f
[build] Concatenate conf files in fat jar.
corwin-of-amber Jul 27, 2021
c06b2bb
[port] Update sbt (1.5.2).
corwin-of-amber Jul 28, 2021
ecdbcd5
[feature] Added `server` CLI command.
corwin-of-amber Jul 28, 2021
998017f
[misc] Logback config for headless mode.
corwin-of-amber Jul 28, 2021
f24e18c
[misc] Set hard max on timeout in server.
corwin-of-amber Jul 28, 2021
1722fe1
[build] Upgraded sbt-assembly (1.0.0).
corwin-of-amber Jul 28, 2021
2c6cb8b
Forwarded submodule.
corwin-of-amber Aug 6, 2021
92ed550
Merge branch 'master' into interactive
corwin-of-amber Apr 25, 2022
da24f8e
[port] `in assembly` syntax is anachronistic.
corwin-of-amber Apr 27, 2022
610f409
[bugfix] Post-merge adjustments.
corwin-of-amber Jun 23, 2022
7710eec
[bugfix] Missing argument in `npm start`.
corwin-of-amber Jun 30, 2022
9c125ca
[feature] Added interval operators to JSON serialization.
corwin-of-amber Jun 30, 2022
70cf634
[port] Bump sbt to 1.5.8.
corwin-of-amber Jun 30, 2022
6c80f5b
[ui] Changed CLI --timeout argument to be in seconds.
corwin-of-amber Jun 30, 2022
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,7 @@ target/
lib_managed/
src_managed/
project/boot/
project/
project/plugins/project/
target/
.history
.cache
.lib/
Expand Down Expand Up @@ -95,9 +94,6 @@ fabric.properties
# Compiled class file
*.class

# Log file
*.log

# BlueJ files
*.ctxt

Expand All @@ -119,9 +115,6 @@ hs_err_pid*
*~
.*.swp

# stats
*.csv

# Emacs-generated
.#*

Expand All @@ -146,10 +139,17 @@ node_modules
/build
/scratch

# logs, stats, and other outputs
/logs
*.log
*.csv
# traces
*.out

# certification results
certify/

*results.tex
trace.json
*.trace.json
*.db.json
3 changes: 3 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[submodule "ext/tutorial"]
path = ext/tutorial
url = https://github.com/TyGuS/suslik-tutorial.git
1 change: 1 addition & 0 deletions Aptfile
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
z3
1 change: 1 addition & 0 deletions Procfile
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
web: target/universal/stage/bin/synthesis-server
38 changes: 23 additions & 15 deletions build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -10,31 +10,38 @@ scalaVersion := "2.12.12"
javacOptions ++= Seq("-source", "1.8", "-target", "1.8", "-Xlint")
scalacOptions += "-target:jvm-1.8"

resolvers in ThisBuild ++= Seq(
ThisBuild / resolvers ++= Seq(
Resolver.sonatypeRepo("releases"),
Resolver.sonatypeRepo("snapshots")
)

resolvers += Resolver.bintrayIvyRepo("com.eed3si9n", "sbt-plugins")

lazy val akkaHttpVersion = "10.2.4"
lazy val akkaVersion = "2.6.14"

libraryDependencies ++= Seq(
"org.slf4j" % "slf4j-api" % "1.6.4" withSources(),
"ch.qos.logback" % "logback-classic" % "1.1.3" % "test",
"org.scalatest" %% "scalatest" % "3.0.1" % "test",
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.6" withSources(),
"org.scala-lang.modules" %% "scala-parser-combinators" % "1.1.2" withSources(),
"org.scalaz" %% "scalaz-core" % "7.2.11",
"com.github.scopt" %% "scopt" % "3.7.0",
"com.typesafe.scala-logging" %% "scala-logging" % "3.7.2",
"com.lihaoyi" %% "upickle" % "0.9.5",
"org.bitbucket.franck44.scalasmt" %% "scalasmt" % "2.1.1-SNAPSHOT" withSources()
"com.lihaoyi" %% "upickle" % "1.3.15",
"org.bitbucket.franck44.scalasmt" %% "scalasmt" % "2.1.1-SNAPSHOT" withSources(),
// Server stuff
"com.typesafe.akka" %% "akka-http" % akkaHttpVersion,
"com.typesafe.akka" %% "akka-stream" % akkaVersion,
"com.typesafe.akka" %% "akka-actor-typed" % akkaVersion
)

scalacOptions ++= Seq()

logLevel in ThisBuild := Level.Warn
ThisBuild / logLevel := Level.Warn

// creating a logger and setting level to warn/whatever for console
initialCommands in console :=
console / initialCommands :=
"""|
| import ch.qos.logback.classic.Logger
| import org.slf4j.LoggerFactory
Expand All @@ -43,15 +50,16 @@ initialCommands in console :=
| root.setLevel(Level.OFF)
| """.stripMargin

mainClass in assembly := Some("org.tygus.suslik.synthesis.SynthesisRunner")

test in assembly := {}
Test / parallelExecution := false

parallelExecution in Test := false
assembly / assemblyJarName := "suslik.jar"
assembly / mainClass := Some("org.tygus.suslik.synthesis.SynthesisRunner")
assembly / test := {}

assemblyJarName in assembly := "suslik.jar"

assemblyMergeStrategy in assembly := {
case PathList("META-INF", xs @ _*) => MergeStrategy.discard
case x => MergeStrategy.first
assembly / assemblyMergeStrategy := {
case PathList("META-INF", _*) => MergeStrategy.discard
case x if Assembly.isConfigFile(x) => MergeStrategy.concat
case _ => MergeStrategy.first
}

enablePlugins(JavaAppPackaging)
2 changes: 1 addition & 1 deletion evaluation.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@

JAVA8 = 'java' # Path to Java8
SUSLIK_JAR = 'suslik.jar' # Path to suslik.jar
TIMEOUT = '-t=120000' # Timeout option for suslik
TIMEOUT = '-t=120' # Timeout option for suslik
TEST_DIR = 'src/test/resources/synthesis/paper-benchmarks/' # Root directory for the tests
VARIANTS = ['phased', 'invert', 'fail', 'commute', 'none'] # Configurations
CSV_IN = 'stats.csv' # Intermediate CSV file produced by suslik
Expand Down
1 change: 1 addition & 0 deletions ext/tutorial
Submodule tutorial added at 2eaf0f
28 changes: 28 additions & 0 deletions logback.prod.xml
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
<?xml version="1.0" encoding="UTF-8"?>
<configuration>
<logger name="org.bitbucket.franck44" level="ERROR"/>

<!-- Stop output INFO at start -->
<statusListener class="ch.qos.logback.core.status.NopStatusListener" />

<appender name="LOGFILE" class="ch.qos.logback.core.rolling.RollingFileAppender">
<file>logs/suslik-server.log</file>
<rollingPolicy class="ch.qos.logback.core.rolling.FixedWindowRollingPolicy">
<fileNamePattern>logs/suslik-server.%i.log.zip</fileNamePattern>
<minIndex>1</minIndex>
<maxIndex>30</maxIndex>
</rollingPolicy>

<triggeringPolicy class="ch.qos.logback.core.rolling.SizeBasedTriggeringPolicy">
<maxFileSize>50MB</maxFileSize>
</triggeringPolicy>
<encoder>
<pattern>%d{yyyy-MM-dd HH:mm:ss} [%thread] %-5level %logger{35} - %msg%n</pattern>
</encoder>
</appender>

<root level="info">
<appender-ref ref="LOGFILE"/>
</root>

</configuration>
Loading