diff --git a/lean4-fringe.el b/lean4-fringe.el
index e5ab9e0..851f6a1 100644
--- a/lean4-fringe.el
+++ b/lean4-fringe.el
@@ -22,7 +22,6 @@
 
 ;;; Code:
 
-(require 'lean4-settings)
 (require 'lsp-mode)
 (require 'lsp-protocol)
 
@@ -70,6 +69,11 @@
 
 (defvar-local lean4-fringe-data nil)
 
+(defcustom lean4-show-file-progress t
+  "Highlight file progress in the current buffer."
+  :group 'lean4
+  :type 'boolean)
+
 (defun lean4-fringe-update-progress-overlays ()
   "Update processing bars in the current buffer."
   (dolist (ov (flatten-tree (overlay-lists)))
diff --git a/lean4-info.el b/lean4-info.el
index 923cf56..37830a7 100644
--- a/lean4-info.el
+++ b/lean4-info.el
@@ -24,7 +24,6 @@
 
 (require 'dash)
 (require 'lean4-syntax)
-(require 'lean4-settings)
 (require 'lsp-mode)
 (require 'lsp-protocol)
 (require 'magit-section)
@@ -100,6 +99,13 @@ The buffer is supposed to be the *Lean Goal* buffer."
       (forward-line (1- line))
       (forward-char column))))
 
+(defcustom lean4-highlight-inaccessible-names t
+  "Use font to highlight inaccessible names.
+Set this variable to t to highlight inaccessible names in the info display
+using `font-lock-comment-face' instead of the `✝` suffix used by Lean."
+  :group 'lean4
+  :type 'boolean)
+
 (defun lean4-info--insert-highlight-inaccessible-names (&rest text)
   (let ((begin (point)))
     (apply #'insert text)
diff --git a/lean4-lake.el b/lean4-lake.el
index bfca627..1d0ced9 100644
--- a/lean4-lake.el
+++ b/lean4-lake.el
@@ -22,7 +22,12 @@
 ;;; Code:
 
 (require 'lean4-util)
-(require 'lean4-settings)
+
+(defcustom lean4-lake-name
+  (if (eq system-type 'windows-nt) "lake.exe" "lake")
+  "Name of lake executable."
+  :group 'lake
+  :type 'string)
 
 (defun lean4-lake-find-dir-in (dir)
   "Find a parent directory of DIR with file \"lakefile.lean\"."
diff --git a/lean4-mode.el b/lean4-mode.el
index 336cd0b..9d6c61a 100644
--- a/lean4-mode.el
+++ b/lean4-mode.el
@@ -49,7 +49,6 @@
 (require 'lean4-fringe)
 (require 'lean4-info)
 (require 'lean4-lake)
-(require 'lean4-settings)
 (require 'lean4-syntax)
 (require 'lean4-util)
 
@@ -69,6 +68,16 @@
 (declare-function lean-mode "ext:lean-mode")
 (declare-function quail-show-key "quail")
 
+(defgroup lean4 nil
+  "Major mode for Lean4 programming language and theorem prover."
+  :group 'languages
+  :link '(info-link :tag "Info Manual" "(lean4-mode)")
+  :link '(url-link
+          :tag "Website"
+          "https://github.com/leanprover-community/lean4-mode")
+  :link '(emacs-library-link :tag "Library Source" "lean4-mode.el")
+  :prefix "lean4-")
+
 (defun lean4-compile-string (lake-name exe-name args file-name)
   "Command to run EXE-NAME with extra ARGS and FILE-NAME.
 If LAKE-NAME is nonempty, then prepend \"LAKE-NAME env\" to the command
@@ -271,6 +280,14 @@ added here because it will be called by `lsp' if the variable
   (interactive)
   (message "Lean %s" (mapconcat #'number-to-string (lean4--version) ".")))
 
+(defcustom lean4-autodetect-lean3 nil
+  "Autodetect Lean version.
+Use elan to check if current project uses Lean 3 or Lean 4 and initialize the
+right mode when visiting a file.  If elan has a default Lean version, Lean files
+outside a project will default to that mode."
+  :group 'lean4
+  :type 'boolean)
+
 ;;;###autoload
 (defun lean4-select-mode ()
   "Automatically select mode (Lean 3 vs Lean 4)."
diff --git a/lean4-settings.el b/lean4-settings.el
deleted file mode 100644
index e8f0f10..0000000
--- a/lean4-settings.el
+++ /dev/null
@@ -1,101 +0,0 @@
-;;; lean4-settings.el --- Lean4-Mode User-Options  -*- lexical-binding: t; -*-
-
-;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-
-;; This file is not part of GNU Emacs.
-
-;; Licensed under the Apache License, Version 2.0 (the "License"); you
-;; may not use this file except in compliance with the License.  You
-;; may obtain a copy of the License at
-;;
-;;     http://www.apache.org/licenses/LICENSE-2.0
-;;
-;; Unless required by applicable law or agreed to in writing, software
-;; distributed under the License is distributed on an "AS IS" BASIS,
-;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
-;; implied.  See the License for the specific language governing
-;; permissions and limitations under the License.
-
-;;; Commentary:
-
-;; This library defines custom variables for `lean4-mode'.
-
-;;; Code:
-
-(require 'lsp-mode)
-
-(defgroup lean4 nil
-  "Major mode for Lean4 programming language and theorem prover."
-  :group 'languages
-  :link '(info-link :tag "Info Manual" "(lean4-mode)")
-  :link '(url-link
-          :tag "Website"
-          "https://github.com/leanprover-community/lean4-mode")
-  :link '(emacs-library-link :tag "Library Source" "lean4-mode.el")
-  :prefix "lean4-")
-
-(defcustom lean4-rootdir nil
-  "Full pathname of lean root directory.  It should be defined by user."
-  :group 'lean4
-  :type 'string)
-
-(defcustom lean4-executable-name
-  (if (eq system-type 'windows-nt) "lean.exe" "lean")
-  "Name of lean executable."
-  :group 'lean4
-  :type 'string)
-
-(defcustom lean4-lake-name
-  (if (eq system-type 'windows-nt) "lake.exe" "lake")
-  "Name of lake executable."
-  :group 'lake
-  :type 'string)
-
-(defcustom lean4-memory-limit 1024
-  "Memory limit for lean process in megabytes."
-  :group 'lean4
-  :type 'number)
-
-(defcustom lean4-timeout-limit 100000
-  "Deterministic timeout limit.
-
-It is approximately the maximum number of memory allocations in thousands."
-  :group 'lean4
-  :type 'number)
-
-(defcustom lean4-extra-arguments nil
-  "Extra command-line arguments to the lean process."
-  :group 'lean4
-  :type '(list string))
-
-(defcustom lean4-delete-trailing-whitespace nil
-  "Automatically delete trailing shitespace.
-Set this variable to true to automatically delete trailing
-whitespace when a buffer is loaded from a file or when it is
-written."
-  :group 'lean4
-  :type 'boolean)
-
-(defcustom lean4-highlight-inaccessible-names t
-  "Use font to highlight inaccessible names.
-Set this variable to t to highlight inaccessible names in the info display
-using `font-lock-comment-face' instead of the `✝` suffix used by Lean."
-  :group 'lean4
-  :type 'boolean)
-
-(defcustom lean4-show-file-progress t
-  "Highlight file progress in the current buffer."
-  :group 'lean4
-  :type 'boolean)
-
-
-(defcustom lean4-autodetect-lean3 nil
-  "Autodetect Lean version.
-Use elan to check if current project uses Lean 3 or Lean 4 and initialize the
-right mode when visiting a file.  If elan has a default Lean version, Lean files
-outside a project will default to that mode."
-  :group 'lean4
-  :type 'boolean)
-
-(provide 'lean4-settings)
-;;; lean4-settings.el ends here
diff --git a/lean4-util.el b/lean4-util.el
index 273a530..79cfa7f 100644
--- a/lean4-util.el
+++ b/lean4-util.el
@@ -23,7 +23,17 @@
 ;;; Code:
 
 (require 'compat)
-(require 'lean4-settings)
+
+(defcustom lean4-executable-name
+  (if (eq system-type 'windows-nt) "lean.exe" "lean")
+  "Name of lean executable."
+  :group 'lean4
+  :type 'string)
+
+(defcustom lean4-rootdir nil
+  "Full pathname of lean root directory.  It should be defined by user."
+  :group 'lean4
+  :type 'string)
 
 (defun lean4-setup-rootdir ()
   "Search for lean executable in variable `exec-path'.
@@ -55,6 +65,14 @@ First try to find an executable named `lean4-executable-name' in
   "Return fullpath of lean executable EXE-NAME."
   (file-name-concat (lean4-get-rootdir) "bin" exe-name))
 
+(defcustom lean4-delete-trailing-whitespace nil
+  "Automatically delete trailing shitespace.
+Set this variable to true to automatically delete trailing
+whitespace when a buffer is loaded from a file or when it is
+written."
+  :group 'lean4
+  :type 'boolean)
+
 (defun lean4-whitespace-cleanup ()
   "Delete trailing whitespace if `lean4-delete-trailing-whitespace' is t."
   (when lean4-delete-trailing-whitespace